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;

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

hence
||.(f | A).|| = ||.f.|| | A
by A4, FUNCT_1:2; :: thesis: verum(||.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;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