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 ;
then c in (dom f) /\ X by ;
then A5: c in dom (f | X) by RELAT_1:61;
thus ((- f) | X) . c = (- f) . c by
.= - (f . c) by VALUED_1:8
.= - ((f | X) . c) by
.= (- (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 ; :: 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 " )) /\ X by Def2
.= ((dom f) /\ X) \ ((f " ) /\ X) by XBOOLE_1:50
.= (dom (f | X)) \ (X /\ (f " )) by RELAT_1:61
.= (dom (f | X)) \ ((f | X) " ) 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
.= (f . c) " by
.= ((f | X) . c) " by
.= ((f | X) ^) . c by A6, A8, Def2 ; :: thesis: verum
end;
hence (f ^) | X = (f | X) ^ by ; :: 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 ;
thus ((abs f) | X) . c = (abs f) . c by
.= |.(f . c).| by VALUED_1:18
.= |.((f | X) . c).| by
.= (abs (f | X)) . c by VALUED_1:18 ; :: thesis: verum
end;
hence (abs f) | X = abs (f | X) by ; :: thesis: verum