let n be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL
for h being PartFunc of REAL,(REAL n) st A c= dom h holds
|.(h | A).| = |.h.| | A
let A be non empty closed_interval Subset of REAL; :: thesis: for h being PartFunc of REAL,(REAL n) st A c= dom h holds
|.(h | A).| = |.h.| | A
let h be PartFunc of REAL,(REAL n); :: thesis: ( A c= dom h implies |.(h | A).| = |.h.| | A )
assume A1: A c= dom h ; :: thesis: |.(h | A).| = |.h.| | A
A2: dom (h | A) = A by A1, RELAT_1:62;
A3: dom (|.h.| | A) = (dom |.h.|) /\ A by RELAT_1:61
.= (dom h) /\ A by NFCONT_4:def 2
.= A by A1, XBOOLE_1:28 ;
A4: dom |.(h | A).| = dom (|.h.| | A) by A3, A2, NFCONT_4:def 2;

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

let x be object ; :: thesis: ( x in dom (|.h.| | A) implies (|.h.| | A) . x = |.(h | A).| . x )
assume A5: x in dom (|.h.| | A) ; :: thesis: (|.h.| | A) . x = |.(h | A).| . x
then A6: x in (dom |.h.|) /\ A by RELAT_1:61;
then A7: x in (dom h) /\ A by NFCONT_4:def 2;
then A8: x in dom (h | A) by RELAT_1:61;
A9: x in dom |.h.| by A6, XBOOLE_0:def 4;
A10: x in dom h by A7, XBOOLE_0:def 4;
A11: h /. x = h . x by A10, PARTFUN1:def 6
.= (h | A) . x by A8, FUNCT_1:47
.= (h | A) /. x by A8, PARTFUN1:def 6 ;
thus (|.h.| | A) . x = |.h.| . x by A6, FUNCT_1:48
.= |.h.| /. x by A9, PARTFUN1:def 6
.= |.(h /. x).| by A9, NFCONT_4:def 2
.= |.(h | A).| /. x by A11, A4, A5, NFCONT_4:def 2
.= |.(h | A).| . x by A4, A5, PARTFUN1:def 6 ; :: thesis: verum

end;

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