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: now :: thesis: for c being object st c in dom ((- f) | X) holds
((- f) | X) . c = (- (f | X)) . c

let c be object ; :: 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 A3: c in (dom (- f)) /\ X by RELAT_1:61;
then c in dom (- f) by XBOOLE_0:def 4;
then A4: c in dom f by VALUED_1:8;
c in X by A3, XBOOLE_0:def 4;
then c in (dom f) /\ X by A4, XBOOLE_0:def 4;
then A5: c in dom (f | X) by RELAT_1:61;
thus ((- f) | X) . c = (- f) . c by A2, FUNCT_1:47
.= - (f . c) by VALUED_1:8
.= - ((f | X) . c) by A5, FUNCT_1:47
.= (- (f | X)) . c by VALUED_1:8 ; :: thesis: verum

end;

dom ((- f) | X) = (dom (- f)) /\ X by RELAT_1:61
.= (dom f) /\ X by VALUED_1:8
.= dom (f | X) by RELAT_1:61
.= dom (- (f | X)) by VALUED_1:8 ;
hence (- f) | X = - (f | X) by A1, FUNCT_1:2; :: thesis: ( (f ^) | X = (f | X) ^ & (abs f) | X = abs (f | X) )
A6: dom ((f ^) | X) = (dom (f ^)) /\ X by RELAT_1:61
.= ((dom f) \ (f " {0})) /\ X by Def2
.= ((dom f) /\ X) \ ((f " {0}) /\ X) by XBOOLE_1:50
.= (dom (f | X)) \ (X /\ (f " {0})) by RELAT_1:61
.= (dom (f | X)) \ ((f | X) " {0}) by FUNCT_1:70
.= dom ((f | X) ^) by Def2 ;
A7: dom ((f | X) ^) c= dom (f | X) by Th1;

now :: thesis: for c being object st c in dom ((f ^) | X) holds
((f ^) | X) . c = ((f | X) ^) . c

let c be object ; :: thesis: ( c in dom ((f ^) | X) implies ((f ^) | X) . c = ((f | X) ^) . c )
assume A8: c in dom ((f ^) | X) ; :: thesis: ((f ^) | X) . c = ((f | X) ^) . c
then c in (dom (f ^)) /\ X by RELAT_1:61;
then A9: c in dom (f ^) by XBOOLE_0:def 4;
thus ((f ^) | X) . c = (f ^) . c by A8, FUNCT_1:47
.= (f . c) " by A9, Def2
.= ((f | X) . c) " by A7, A6, A8, FUNCT_1:47
.= ((f | X) ^) . c by A6, A8, Def2 ; :: thesis: verum

end;

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

now :: thesis: for c being object st c in dom ((abs f) | X) holds
((abs f) | X) . c = (abs (f | X)) . c

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

end;

hence (abs f) | X = abs (f | X) by A10, FUNCT_1:2; :: thesis: verum