let X be set ; :: thesis: for S, T being RealNormSpace
for f being PartFunc of S,T holds ||.f.|| | X = ||.(f | X).||
let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T holds ||.f.|| | X = ||.(f | X).||
let f be PartFunc of S,T; :: thesis: ||.f.|| | X = ||.(f | X).||
A1: 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 Point of S st c in dom (||.f.|| | X) holds
(||.f.|| | X) . c = ||.(f | X).|| . c
let c be Point of S; :: 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 A1, NORMSP_0:def 3;
c in (dom ||.f.||) /\ X by A2, RELAT_1:61;
then A4: c in dom ||.f.|| by XBOOLE_0:def 4;
thus (||.f.|| | X) . c = ||.f.|| . c by A2, FUNCT_1:47
.= ||.(f /. c).|| by A4, NORMSP_0:def 3
.= ||.((f | X) /. c).|| by A3, PARTFUN2:15
.= ||.(f | X).|| . c by A1, A2, NORMSP_0:def 3 ; :: thesis: verum
end;
hence ||.f.|| | X = ||.(f | X).|| by A1, PARTFUN1:5; :: thesis: verum