let CNS1, CNS2 be ComplexNormSpace; :: thesis: for X being set
for f being PartFunc of CNS1,CNS2 holds ||.f.|| | X = ||.(f | X).||
let X be set ; :: thesis: for f being PartFunc of CNS1,CNS2 holds ||.f.|| | X = ||.(f | X).||
let f be PartFunc of CNS1,CNS2; :: thesis: ||.f.|| | X = ||.(f | X).||
A1: dom (||.f.|| | X) = (dom ||.f.||) /\ X by RELAT_1:90
.= (dom f) /\ X by Def2
.= dom (f | X) by RELAT_1:90
.= dom ||.(f | X).|| by Def2 ;

now

let c be Point of CNS1; :: 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;
A4: c in dom (f | X) by A1, A2, Def2;
thus (||.f.|| | X) . c = ||.f.|| . c by A2, FUNCT_1:70
.= ||.(f /. c).|| by A3, Def2
.= ||.((f | X) /. c).|| by A4, PARTFUN2:32
.= ||.(f | X).|| . c by A1, A2, Def2 ; :: thesis: verum

end;

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