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) )

.= (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;

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 ;

( (- 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

dom ((- f) | X) =
(dom (- f)) /\ X
by RELAT_1:61
((- 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;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

.= (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

hence
(f ^) | X = (f | X) ^
by A6, FUNCT_1:2; :: thesis: (abs f) | X = abs (f | X)((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;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

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

hence
(abs f) | X = abs (f | X)
by A10, FUNCT_1:2; :: thesis: verum((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;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