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 ;
A3: dom (|.h.| | A) = () /\ A by RELAT_1:61
.= (dom h) /\ A by NFCONT_4:def 2
.= A by ;
A4: dom |.(h | A).| = dom (|.h.| | A) by ;
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 () /\ 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 ;
A10: x in dom h by ;
A11: h /. x = h . x by
.= (h | A) . x by
.= (h | A) /. x by ;
thus (|.h.| | A) . x = |.h.| . x by
.= |.h.| /. x by
.= |.(h /. x).| by
.= |.(h | A).| /. x by
.= |.(h | A).| . x by ; :: thesis: verum
end;
hence |.(h | A).| = |.h.| | A by ; :: thesis: verum