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