let M be non empty set ; :: thesis: for V being ComplexNormSpace

for f being PartFunc of M,V

for X being set holds

( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )

let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V

for X being set holds

( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )

let f be PartFunc of M,V; :: thesis: for X being set holds

( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )

let X be set ; :: thesis: ( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )

.= (dom f) /\ X by VFUNCT_1:def 5

.= dom (f | X) by RELAT_1:61

.= dom (- (f | X)) by VFUNCT_1:def 5 ;

hence (- f) | X = - (f | X) by A1, PARTFUN2:1; :: thesis: ||.f.|| | X = ||.(f | X).||

A8: dom (||.f.|| | X) = (dom ||.f.||) /\ X by RELAT_1:61

.= (dom f) /\ X by NORMSP_0:def 3

.= dom (f | X) by RELAT_1:61

.= dom ||.(f | X).|| by NORMSP_0:def 3 ;

for f being PartFunc of M,V

for X being set holds

( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )

let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V

for X being set holds

( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )

let f be PartFunc of M,V; :: thesis: for X being set holds

( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )

let X be set ; :: thesis: ( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )

A1: now :: thesis: for c being Element of M 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 Element of M; :: 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 A4: c in X by XBOOLE_0:def 4;

A5: c in dom (- f) by A3, XBOOLE_0:def 4;

then c in dom f by VFUNCT_1:def 5;

then c in (dom f) /\ X by A4, XBOOLE_0:def 4;

then A6: c in dom (f | X) by RELAT_1:61;

then A7: c in dom (- (f | X)) by VFUNCT_1:def 5;

thus ((- f) | X) /. c = (- f) /. c by A2, PARTFUN2:15

.= - (f /. c) by A5, VFUNCT_1:def 5

.= - ((f | X) /. c) by A6, PARTFUN2:15

.= (- (f | X)) /. c by A7, VFUNCT_1:def 5 ; :: 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 A4: c in X by XBOOLE_0:def 4;

A5: c in dom (- f) by A3, XBOOLE_0:def 4;

then c in dom f by VFUNCT_1:def 5;

then c in (dom f) /\ X by A4, XBOOLE_0:def 4;

then A6: c in dom (f | X) by RELAT_1:61;

then A7: c in dom (- (f | X)) by VFUNCT_1:def 5;

thus ((- f) | X) /. c = (- f) /. c by A2, PARTFUN2:15

.= - (f /. c) by A5, VFUNCT_1:def 5

.= - ((f | X) /. c) by A6, PARTFUN2:15

.= (- (f | X)) /. c by A7, VFUNCT_1:def 5 ; :: thesis: verum

.= (dom f) /\ X by VFUNCT_1:def 5

.= dom (f | X) by RELAT_1:61

.= dom (- (f | X)) by VFUNCT_1:def 5 ;

hence (- f) | X = - (f | X) by A1, PARTFUN2:1; :: thesis: ||.f.|| | X = ||.(f | X).||

A8: dom (||.f.|| | X) = (dom ||.f.||) /\ X by RELAT_1:61

.= (dom f) /\ X by NORMSP_0:def 3

.= dom (f | X) by RELAT_1:61

.= dom ||.(f | X).|| by NORMSP_0:def 3 ;

now :: thesis: for c being Element of M st c in dom (||.f.|| | X) holds

(||.f.|| | X) . c = ||.(f | X).|| . c

hence
||.f.|| | X = ||.(f | X).||
by A8, PARTFUN1:5; :: thesis: verum(||.f.|| | X) . c = ||.(f | X).|| . c

let c be Element of M; :: thesis: ( c in dom (||.f.|| | X) implies (||.f.|| | X) . c = ||.(f | X).|| . c )

assume A9: c in dom (||.f.|| | X) ; :: thesis: (||.f.|| | X) . c = ||.(f | X).|| . c

then A10: c in dom (f | X) by A8, NORMSP_0:def 3;

c in (dom ||.f.||) /\ X by A9, RELAT_1:61;

then A11: c in dom ||.f.|| by XBOOLE_0:def 4;

thus (||.f.|| | X) . c = ||.f.|| . c by A9, FUNCT_1:47

.= ||.(f /. c).|| by A11, NORMSP_0:def 3

.= ||.((f | X) /. c).|| by A10, PARTFUN2:15

.= ||.(f | X).|| . c by A8, A9, NORMSP_0:def 3 ; :: thesis: verum

end;assume A9: c in dom (||.f.|| | X) ; :: thesis: (||.f.|| | X) . c = ||.(f | X).|| . c

then A10: c in dom (f | X) by A8, NORMSP_0:def 3;

c in (dom ||.f.||) /\ X by A9, RELAT_1:61;

then A11: c in dom ||.f.|| by XBOOLE_0:def 4;

thus (||.f.|| | X) . c = ||.f.|| . c by A9, FUNCT_1:47

.= ||.(f /. c).|| by A11, NORMSP_0:def 3

.= ||.((f | X) /. c).|| by A10, PARTFUN2:15

.= ||.(f | X).|| . c by A8, A9, NORMSP_0:def 3 ; :: thesis: verum