let D be non empty set ; :: thesis: for H1, H2 being Functional_Sequence of D,REAL
for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds
for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
let H1, H2 be Functional_Sequence of D,REAL; :: thesis: for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds
for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
let X be set ; :: thesis: ( H1 is_point_conv_on X & H2 is_point_conv_on X implies for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) )
assume ( H1 is_point_conv_on X & H2 is_point_conv_on X ) ; :: thesis: for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
then ( X common_on_dom H1 & X common_on_dom H2 ) by Def12;
hence for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) by Th32; :: thesis: verum