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:61
.= ((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:61
.= (dom (f | X)) \ ((f | X) " {0c}) by FUNCT_1:70
.= dom ((f | X) ^) by Def2 ;
A2: now :: thesis: for c being Element of C st c in dom ((- f) | X) holds
((- f) | X) /. c = (- (f | X)) /. c
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:61;
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 Th5;
then c in (dom f) /\ X by A5, XBOOLE_0:def 4;
then A7: c in dom (f | X) by RELAT_1:61;
then A8: c in dom (- (f | X)) by Th5;
thus ((- f) | X) /. c = (- f) /. c by A3, PARTFUN2:15
.= - (f /. c) by A6, Th5
.= - ((f | X) /. c) by A7, PARTFUN2:15
.= (- (f | X)) /. c by A8, Th5 ; :: thesis: verum
end;
dom ((- f) | X) = (dom (- f)) /\ X by RELAT_1:61
.= (dom f) /\ X by Th5
.= dom (f | X) by RELAT_1:61
.= dom (- (f | X)) by Th5 ;
hence (- f) | X = - (f | X) by A2, PARTFUN2:1; :: thesis: ( (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )
A9: dom ((f | X) ^) c= dom (f | X) by Th6;
now :: thesis: for c being Element of C st c in dom ((f ^) | X) holds
((f ^) | X) /. c = ((f | X) ^) /. c
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:61;
then A11: c in dom (f ^) by XBOOLE_0:def 4;
thus ((f ^) | X) /. c = (f ^) /. c by A10, PARTFUN2:15
.= (f /. c) " by A11, Def2
.= ((f | X) /. c) " by A9, A1, A10, PARTFUN2:15
.= ((f | X) ^) /. c by A1, A10, Def2 ; :: thesis: verum
end;
hence (f ^) | X = (f | X) ^ by A1, PARTFUN2:1; :: thesis: |.f.| | X = |.(f | X).|
A12: dom (|.f.| | X) = (dom |.f.|) /\ X by RELAT_1:61
.= (dom f) /\ X by VALUED_1:def 11
.= dom (f | X) by RELAT_1:61
.= dom |.(f | X).| by VALUED_1:def 11 ;
now :: thesis: for c being Element of C st c in dom (|.f.| | X) holds
(|.f.| | X) . c = |.(f | X).| . c
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:61;
then A16: c in dom |.f.| by XBOOLE_0:def 4;
thus (|.f.| | X) . c = |.f.| . c by A14, FUNCT_1:47
.= |.(f . c).| by VALUED_1:18
.= |.(f /. c).| by A16, A13, PARTFUN1:def 6
.= |.((f | X) /. c).| by A15, PARTFUN2:15
.= |.((f | X) . c).| by A15, PARTFUN1:def 6
.= |.(f | X).| . c by VALUED_1:18 ; :: thesis: verum
end;
hence |.f.| | X = |.(f | X).| by A12, PARTFUN1:5; :: thesis: verum