let X be set ; :: thesis: for C being non empty set
for f being PartFunc of C,COMPLEX holds
( (- f) | X = - (f | X) & (f ^ ) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )
let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds
( (- f) | X = - (f | X) & (f ^ ) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )
let f be PartFunc of C,COMPLEX ; :: thesis: ( (- f) | X = - (f | X) & (f ^ ) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )
A1: dom ((f ^ ) | X) = (dom (f ^ )) /\ X by RELAT_1:90
.= ((dom f) \ (f " {0c })) /\ X by Def2
.= ((dom f) /\ X) \ ((f " {0c }) /\ X) by XBOOLE_1:50
.= (dom (f | X)) \ (X /\ (f " {0c })) by RELAT_1:90
.= (dom (f | X)) \ ((f | X) " {0c }) by FUNCT_1:139
.= dom ((f | X) ^ ) by Def2 ;

A2: now

let c be Element of C; :: thesis: ( c in dom ((- f) | X) implies ((- f) | X) /. c = (- (f | X)) /. c )
assume A3: c in dom ((- f) | X) ; :: thesis: ((- f) | X) /. c = (- (f | X)) /. c
then A4: c in (dom (- f)) /\ X by RELAT_1:90;
then A5: c in X by XBOOLE_0:def 4;
A6: c in dom (- f) by A4, XBOOLE_0:def 4;
then c in dom f by Th9;
then c in (dom f) /\ X by A5, XBOOLE_0:def 4;
then A7: c in dom (f | X) by RELAT_1:90;
then A8: c in dom (- (f | X)) by Th9;
thus ((- f) | X) /. c = (- f) /. c by A3, PARTFUN2:32
.= - (f /. c) by A6, Th9
.= - ((f | X) /. c) by A7, PARTFUN2:32
.= (- (f | X)) /. c by A8, Th9 ; :: thesis: verum

end;

dom ((- f) | X) = (dom (- f)) /\ X by RELAT_1:90
.= (dom f) /\ X by Th9
.= dom (f | X) by RELAT_1:90
.= dom (- (f | X)) by Th9 ;
hence (- f) | X = - (f | X) by A2, PARTFUN2:3; :: thesis: ( (f ^ ) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )
A9: dom ((f | X) ^ ) c= dom (f | X) by Th15;

now

let c be Element of C; :: thesis: ( c in dom ((f ^ ) | X) implies ((f ^ ) | X) /. c = ((f | X) ^ ) /. c )
assume A10: c in dom ((f ^ ) | X) ; :: thesis: ((f ^ ) | X) /. c = ((f | X) ^ ) /. c
then c in (dom (f ^ )) /\ X by RELAT_1:90;
then A11: c in dom (f ^ ) by XBOOLE_0:def 4;
thus ((f ^ ) | X) /. c = (f ^ ) /. c by A10, PARTFUN2:32
.= (f /. c) " by A11, Def2
.= ((f | X) /. c) " by A9, A1, A10, PARTFUN2:32
.= ((f | X) ^ ) /. c by A1, A10, Def2 ; :: thesis: verum

end;

hence (f ^ ) | X = (f | X) ^ by A1, PARTFUN2:3; :: thesis: |.f.| | X = |.(f | X).|
A12: dom (|.f.| | X) = (dom |.f.|) /\ X by RELAT_1:90
.= (dom f) /\ X by VALUED_1:def 11
.= dom (f | X) by RELAT_1:90
.= dom |.(f | X).| by VALUED_1:def 11 ;

now

let c be Element of C; :: thesis: ( c in dom (|.f.| | X) implies (|.f.| | X) . c = |.(f | X).| . c )
A13: dom |.f.| = dom f by VALUED_1:def 11;
assume A14: c in dom (|.f.| | X) ; :: thesis: (|.f.| | X) . c = |.(f | X).| . c
then A15: c in dom (f | X) by A12, VALUED_1:def 11;
c in (dom |.f.|) /\ X by A14, RELAT_1:90;
then A16: c in dom |.f.| by XBOOLE_0:def 4;
thus (|.f.| | X) . c = |.f.| . c by A14, FUNCT_1:70
.= |.(f . c).| by VALUED_1:18
.= |.(f /. c).| by A16, A13, PARTFUN1:def 8
.= |.((f | X) /. c).| by A15, PARTFUN2:32
.= |.((f | X) . c).| by A15, PARTFUN1:def 8
.= |.(f | X).| . c by VALUED_1:18 ; :: thesis: verum

end;

hence |.f.| | X = |.(f | X).| by A12, PARTFUN1:34; :: thesis: verum