let D be non empty set ; :: thesis: for H being Functional_Sequence of D,REAL
for X being set st X common_on_dom H 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 X common_on_dom H 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: ( X common_on_dom H implies for x being Element of D st x in X holds
( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) ) )
assume A1: X common_on_dom H ; :: thesis: for x being Element of D st x in X holds
( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) )
let x be Element of D; :: thesis: ( x in X implies ( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) ) )
assume x in X ; :: thesis: ( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) )
then {x} common_on_dom H by A1, Th27;
hence ( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) ) by Th30; :: thesis: verum