let S, T, U be RealNormSpace; for R1 being RestFunc of S,T st R1 /. (0. S) = 0. T holds
for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is RestFunc of S,U
let R1 be RestFunc of S,T; ( R1 /. (0. S) = 0. T implies for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is RestFunc of S,U )
assume A1:
R1 /. (0. S) = 0. T
; for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is RestFunc of S,U
let R2 be RestFunc of T,U; ( R2 /. (0. T) = 0. U implies R2 * R1 is RestFunc of S,U )
assume A2:
R2 /. (0. T) = 0. U
; R2 * R1 is RestFunc of S,U
R2 is total
by NDIFF_1:def 5;
then
dom R2 = the carrier of T
by PARTFUN1:def 2;
then A3:
rng R1 c= dom R2
;
A4:
R1 is total
by NDIFF_1:def 5;
then A5:
dom R1 = the carrier of S
by PARTFUN1:def 2;
A6:
now for e0 being Real st e0 > 0 holds
ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 ) )consider d1 being
Real such that A7:
0 < d1
and A8:
for
h being
Point of
S st
||.h.|| < d1 holds
||.(R1 /. h).|| <= 1
* ||.h.||
by A1, Th7;
let e0 be
Real;
( e0 > 0 implies ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 ) ) )assume A9:
e0 > 0
;
ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 ) )set e =
e0 / 2;
A10:
e0 / 2
< e0
by A9, XREAL_1:216;
e0 / 2
> 0
by A9, XREAL_1:215;
then consider d2 being
Real such that A11:
0 < d2
and A12:
for
z being
Point of
T st
||.z.|| < d2 holds
||.(R2 /. z).|| <= (e0 / 2) * ||.z.||
by A2, Th7;
set d =
min (
d1,
d2);
A13:
min (
d1,
d2)
<= d2
by XXREAL_0:17;
A14:
min (
d1,
d2)
<= d1
by XXREAL_0:17;
A15:
now for h being Point of S st h <> 0. S & ||.h.|| < min (d1,d2) holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0let h be
Point of
S;
( h <> 0. S & ||.h.|| < min (d1,d2) implies (||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 )assume that A16:
h <> 0. S
and A17:
||.h.|| < min (
d1,
d2)
;
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0
||.h.|| < d1
by A14, A17, XXREAL_0:2;
then A18:
||.(R1 /. h).|| <= 1
* ||.h.||
by A8;
then
||.(R1 /. h).|| < min (
d1,
d2)
by A17, XXREAL_0:2;
then
||.(R1 /. h).|| < d2
by A13, XXREAL_0:2;
then A19:
||.(R2 /. (R1 /. h)).|| <= (e0 / 2) * ||.(R1 /. h).||
by A12;
(e0 / 2) * ||.(R1 /. h).|| <= (e0 / 2) * ||.h.||
by A9, A18, XREAL_1:64;
then A20:
||.(R2 /. (R1 /. h)).|| <= (e0 / 2) * ||.h.||
by A19, XXREAL_0:2;
A21:
||.h.|| <> 0
by A16, NORMSP_0:def 5;
then
||.h.|| > 0
by NORMSP_1:4;
then
(||.h.|| ") * ||.(R2 /. (R1 /. h)).|| <= (||.h.|| ") * ((e0 / 2) * ||.h.||)
by A20, XREAL_1:64;
then
(||.h.|| ") * ||.(R2 /. (R1 /. h)).|| <= ((||.h.|| ") * ||.h.||) * (e0 / 2)
;
then A22:
(||.h.|| ") * ||.(R2 /. (R1 /. h)).|| <= 1
* (e0 / 2)
by A21, XCMPLX_0:def 7;
R2 /. (R1 /. h) = (R2 * R1) /. h
by A5, A3, PARTFUN2:5;
hence
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0
by A10, A22, XXREAL_0:2;
verum end;
0 < min (
d1,
d2)
by A11, A7, XXREAL_0:15;
hence
ex
d being
Real st
(
d > 0 & ( for
h being
Point of
S st
h <> 0. S &
||.h.|| < d holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 ) )
by A15;
verum end;
dom (R2 * R1) =
dom R1
by A3, RELAT_1:27
.=
the carrier of S
by A4, PARTFUN1:def 2
;
then
R2 * R1 is total
by PARTFUN1:def 2;
hence
R2 * R1 is RestFunc of S,U
by A6, NDIFF_1:23; verum