let Z be RealNormSpace; :: thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of Z st A c= dom f holds
||.(f | A).|| = ||.f.|| | A
let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL, the carrier of Z st A c= dom f holds
||.(f | A).|| = ||.f.|| | A
let f be PartFunc of REAL, the carrier of Z; :: thesis: ( A c= dom f implies ||.(f | A).|| = ||.f.|| | A )
assume A1: A c= dom f ; :: thesis: ||.(f | A).|| = ||.f.|| | A
then A2: dom (f | A) = A by RELAT_1:62;
A3: dom (||.f.|| | A) = (dom ||.f.||) /\ A by RELAT_1:61;
then A6: dom (||.f.|| | A) = (dom f) /\ A by NORMSP_0:def 3;
then dom (||.f.|| | A) = A by A1, XBOOLE_1:28;
then A4: dom ||.(f | A).|| = dom (||.f.|| | A) by A2, NORMSP_0:def 3;

now :: thesis: for x being object st x in dom (||.f.|| | A) holds
(||.f.|| | A) . x = ||.(f | A).|| . x

let x be object ; :: thesis: ( x in dom (||.f.|| | A) implies (||.f.|| | A) . x = ||.(f | A).|| . x )
assume A5: x in dom (||.f.|| | A) ; :: thesis: (||.f.|| | A) . x = ||.(f | A).|| . x
then A9: ( x in dom ||.f.|| & x in dom f ) by A3, A6, XBOOLE_0:def 4;
then A11: f /. x = f . x by PARTFUN1:def 6
.= (f | A) . x by FUNCT_1:49, A5
.= (f | A) /. x by A2, PARTFUN1:def 6, A5 ;
thus (||.f.|| | A) . x = ||.f.|| . x by FUNCT_1:49, A5
.= ||.(f /. x).|| by A9, NORMSP_0:def 3
.= ||.(f | A).|| . x by A11, A4, A5, NORMSP_0:def 3 ; :: thesis: verum

end;

hence ||.(f | A).|| = ||.f.|| | A by A4, FUNCT_1:2; :: thesis: verum