let X be set ; :: thesis: for f being complex-valued Function holds
( (- f) | X = - (f | X) & (f ^ ) | X = (f | X) ^ & (abs f) | X = abs (f | X) )
let f be complex-valued Function; :: thesis: ( (- f) | X = - (f | X) & (f ^ ) | X = (f | X) ^ & (abs f) | X = abs (f | X) )
A1: dom ((- f) | X) = (dom (- f)) /\ X by RELAT_1:90
.= (dom f) /\ X by VALUED_1:8
.= dom (f | X) by RELAT_1:90
.= dom (- (f | X)) by VALUED_1:8 ;

now

let c be set ; :: thesis: ( c in dom ((- f) | X) implies ((- f) | X) . c = (- (f | X)) . c )
assume A2: c in dom ((- f) | X) ; :: thesis: ((- f) | X) . c = (- (f | X)) . c
then c in (dom (- f)) /\ X by RELAT_1:90;
then A3: ( c in dom (- f) & c in X ) by XBOOLE_0:def 4;
then c in dom f by VALUED_1:8;
then c in (dom f) /\ X by A3, XBOOLE_0:def 4;
then A4: c in dom (f | X) by RELAT_1:90;
thus ((- f) | X) . c = (- f) . c by A2, FUNCT_1:70
.= - (f . c) by VALUED_1:8
.= - ((f | X) . c) by A4, FUNCT_1:70
.= (- (f | X)) . c by VALUED_1:8 ; :: thesis: verum

end;

hence (- f) | X = - (f | X) by A1, FUNCT_1:9; :: thesis: ( (f ^ ) | X = (f | X) ^ & (abs f) | X = abs (f | X) )
A5: dom ((f | X) ^ ) c= dom (f | X) by Th11;
A6: dom ((f ^ ) | X) = (dom (f ^ )) /\ X by RELAT_1:90
.= ((dom f) \ (f " {0 })) /\ X by Def8
.= ((dom f) /\ X) \ ((f " {0 }) /\ X) by XBOOLE_1:50
.= (dom (f | X)) \ (X /\ (f " {0 })) by RELAT_1:90
.= (dom (f | X)) \ ((f | X) " {0 }) by FUNCT_1:139
.= dom ((f | X) ^ ) by Def8 ;

now

let c be set ; :: thesis: ( c in dom ((f ^ ) | X) implies ((f ^ ) | X) . c = ((f | X) ^ ) . c )
assume A7: c in dom ((f ^ ) | X) ; :: thesis: ((f ^ ) | X) . c = ((f | X) ^ ) . c
then c in (dom (f ^ )) /\ X by RELAT_1:90;
then A8: ( c in dom (f ^ ) & c in X ) by XBOOLE_0:def 4;
thus ((f ^ ) | X) . c = (f ^ ) . c by A7, FUNCT_1:70
.= (f . c) " by A8, Def8
.= ((f | X) . c) " by A5, A6, A7, FUNCT_1:70
.= ((f | X) ^ ) . c by A6, A7, Def8 ; :: thesis: verum

end;

hence (f ^ ) | X = (f | X) ^ by A6, FUNCT_1:9; :: thesis: (abs f) | X = abs (f | X)
A9: dom ((abs f) | X) = (dom (abs f)) /\ X by RELAT_1:90
.= (dom f) /\ X by VALUED_1:def 11
.= dom (f | X) by RELAT_1:90
.= dom (abs (f | X)) by VALUED_1:def 11 ;

now

let c be set ; :: thesis: ( c in dom ((abs f) | X) implies ((abs f) | X) . c = (abs (f | X)) . c )
assume A10: c in dom ((abs f) | X) ; :: thesis: ((abs f) | X) . c = (abs (f | X)) . c
then A11: c in dom (f | X) by A9, VALUED_1:def 11;
thus ((abs f) | X) . c = (abs f) . c by A10, FUNCT_1:70
.= abs (f . c) by VALUED_1:18
.= abs ((f | X) . c) by A11, FUNCT_1:70
.= (abs (f | X)) . c by VALUED_1:18 ; :: thesis: verum

end;

hence (abs f) | X = abs (f | X) by A9, FUNCT_1:9; :: thesis: verum