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

now

let c be Element of C; :: 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 Th9;
then c in (dom f) /\ X by A3, XBOOLE_0:def 4;
then A4: c in dom (f | X) by RELAT_1:90;
then A5: c in dom (- (f | X)) by Th9;
thus ((- f) | X) /. c = (- f) /. c by A2, PARTFUN2:32
.= - (f /. c) by A3, Th9
.= - ((f | X) /. c) by A4, PARTFUN2:32
.= (- (f | X)) /. c by A5, Th9 ; :: thesis: verum

end;

hence (- f) | X = - (f | X) by A1, PARTFUN2:3; :: thesis: ( (f ^ ) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )
A6: dom ((f | X) ^ ) c= dom (f | X) by Th15;
A7: 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 ;

now

let c be Element of C; :: 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:90;
then A9: ( c in dom (f ^ ) & c in X ) by XBOOLE_0:def 4;
thus ((f ^ ) | X) /. c = (f ^ ) /. c by A8, PARTFUN2:32
.= (f /. c) " by A9, Def2
.= ((f | X) /. c) " by A6, A7, A8, PARTFUN2:32
.= ((f | X) ^ ) /. c by A7, A8, Def2 ; :: thesis: verum

end;

hence (f ^ ) | X = (f | X) ^ by A7, PARTFUN2:3; :: thesis: |.f.| | X = |.(f | X).|
A10: 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 )
assume A11: c in dom (|.f.| | X) ; :: thesis: (|.f.| | X) . c = |.(f | X).| . c
then c in (dom |.f.|) /\ X by RELAT_1:90;
then A12: ( c in dom |.f.| & c in X ) by XBOOLE_0:def 4;
A13: c in dom (f | X) by A10, A11, VALUED_1:def 11;
A14: dom |.f.| = dom f by VALUED_1:def 11;
thus (|.f.| | X) . c = |.f.| . c by A11, FUNCT_1:70
.= |.(f . c).| by VALUED_1:18
.= |.(f /. c).| by A12, A14, PARTFUN1:def 8
.= |.((f | X) /. c).| by A13, PARTFUN2:32
.= |.((f | X) . c).| by A13, PARTFUN1:def 8
.= |.(f | X).| . c by VALUED_1:18 ; :: thesis: verum

end;

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