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;

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

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