let I be Function of REAL,(REAL 1); :: thesis: for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds

( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) )

let J be Function of (REAL 1),REAL; :: thesis: ( I = (proj (1,1)) " & J = proj (1,1) implies ( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) ) )

assume that

A1: I = (proj (1,1)) " and

A2: J = proj (1,1) ; :: thesis: ( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) )

thus for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) :: thesis: for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1)

( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) )

let J be Function of (REAL 1),REAL; :: thesis: ( I = (proj (1,1)) " & J = proj (1,1) implies ( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) ) )

assume that

A1: I = (proj (1,1)) " and

A2: J = proj (1,1) ; :: thesis: ( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) )

thus for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) :: thesis: for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1)

proof

thus
for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1)
:: thesis: verum
let R be RestFunc; :: thesis: (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1)

R is total by FDIFF_1:def 2;

then reconsider R0 = R as Function of REAL,REAL ;

A3: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

then reconsider R1 = (I * R0) * J as PartFunc of (REAL-NS 1),(REAL-NS 1) ;

for h being non-zero 0. (REAL-NS 1) -convergent sequence of (REAL-NS 1) holds

( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS 1) )

end;R is total by FDIFF_1:def 2;

then reconsider R0 = R as Function of REAL,REAL ;

A3: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

then reconsider R1 = (I * R0) * J as PartFunc of (REAL-NS 1),(REAL-NS 1) ;

for h being non-zero 0. (REAL-NS 1) -convergent sequence of (REAL-NS 1) holds

( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS 1) )

proof

hence
(I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1)
by A3, NDIFF_1:def 10; :: thesis: verum
let h be non-zero 0. (REAL-NS 1) -convergent sequence of (REAL-NS 1); :: thesis: ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS 1) )

A4: lim h = 0. (REAL-NS 1) by NDIFF_1:def 4;

deffunc H_{1}( Nat) -> set = J . (h . $1);

consider s being Real_Sequence such that

A5: for n being Nat holds s . n = H_{1}(n)
from SEQ_1:sch 1();

A6: h is convergent by NDIFF_1:def 4;

then A12: lim s = 0 by A7, SEQ_2:def 7;

then reconsider s = s as non-zero 0 -convergent Real_Sequence by A11, A12, FDIFF_1:def 1;

A15: J * I = id REAL by A1, A2, Lm1, FUNCT_1:39;

A24: lim ((s ") (#) (R /* s)) = 0 by FDIFF_1:def 2;

A25: (s ") (#) (R /* s) is convergent by FDIFF_1:def 2;

then lim |.((s ") (#) (R /* s)).| = |.(lim ((s ") (#) (R /* s))).| by SEQ_4:14;

then A26: lim |.((s ") (#) (R /* s)).| = 0 by A24, ABSVALUE:2;

A27: abs ((s ") (#) (R /* s)) is convergent by A25, SEQ_4:13;

hence ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS 1) ) by A28, NORMSP_1:def 7; :: thesis: verum

end;A4: lim h = 0. (REAL-NS 1) by NDIFF_1:def 4;

deffunc H

consider s being Real_Sequence such that

A5: for n being Nat holds s . n = H

A6: h is convergent by NDIFF_1:def 4;

A7: now :: thesis: for p being Real st 0 < p holds

ex m being Nat st

for n being Nat st m <= n holds

|.((s . n) - 0).| < p

then A11:
s is convergent
by SEQ_2:def 6;ex m being Nat st

for n being Nat st m <= n holds

|.((s . n) - 0).| < p

let p be Real; :: thesis: ( 0 < p implies ex m being Nat st

for n being Nat st m <= n holds

|.((s . n) - 0).| < p )

assume 0 < p ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

|.((s . n) - 0).| < p

then consider m being Nat such that

A8: for n being Nat st m <= n holds

||.((h . n) - (0. (REAL-NS 1))).|| < p by A6, A4, NORMSP_1:def 7;

reconsider m = m as Nat ;

take m = m; :: thesis: for n being Nat st m <= n holds

|.((s . n) - 0).| < p

|.((s . n) - 0).| < p ; :: thesis: verum

end;for n being Nat st m <= n holds

|.((s . n) - 0).| < p )

assume 0 < p ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

|.((s . n) - 0).| < p

then consider m being Nat such that

A8: for n being Nat st m <= n holds

||.((h . n) - (0. (REAL-NS 1))).|| < p by A6, A4, NORMSP_1:def 7;

reconsider m = m as Nat ;

take m = m; :: thesis: for n being Nat st m <= n holds

|.((s . n) - 0).| < p

now :: thesis: for n being Nat st m <= n holds

|.((s . n) - 0).| < p

hence
for n being Nat st m <= n holds |.((s . n) - 0).| < p

let n be Nat; :: thesis: ( m <= n implies |.((s . n) - 0).| < p )

assume A9: m <= n ; :: thesis: |.((s . n) - 0).| < p

reconsider nn = n as Nat ;

||.((h . nn) - (0. (REAL-NS 1))).|| < p by A8, A9;

then A10: ||.(h . nn).|| < p by RLVECT_1:13;

s . n = J . (h . n) by A5;

hence |.((s . n) - 0).| < p by A2, A10, Th4; :: thesis: verum

end;assume A9: m <= n ; :: thesis: |.((s . n) - 0).| < p

reconsider nn = n as Nat ;

||.((h . nn) - (0. (REAL-NS 1))).|| < p by A8, A9;

then A10: ||.(h . nn).|| < p by RLVECT_1:13;

s . n = J . (h . n) by A5;

hence |.((s . n) - 0).| < p by A2, A10, Th4; :: thesis: verum

|.((s . n) - 0).| < p ; :: thesis: verum

then A12: lim s = 0 by A7, SEQ_2:def 7;

now :: thesis: for x being object st x in NAT holds

s . x <> 0

then
s is non-zero
by SEQ_1:4;s . x <> 0

let x be object ; :: thesis: ( x in NAT implies s . x <> 0 )

assume x in NAT ; :: thesis: s . x <> 0

then reconsider n = x as Element of NAT ;

A13: 0 <= |.(s . n).| by COMPLEX1:46;

h . n <> 0. (REAL-NS 1) by NDIFF_1:6;

then A14: ||.(h . n).|| <> 0 by NORMSP_0:def 5;

s . n = J . (h . n) by A5;

then |.(s . x).| <> 0 by A2, A14, Th4;

hence s . x <> 0 by A13, COMPLEX1:47; :: thesis: verum

end;assume x in NAT ; :: thesis: s . x <> 0

then reconsider n = x as Element of NAT ;

A13: 0 <= |.(s . n).| by COMPLEX1:46;

h . n <> 0. (REAL-NS 1) by NDIFF_1:6;

then A14: ||.(h . n).|| <> 0 by NORMSP_0:def 5;

s . n = J . (h . n) by A5;

then |.(s . x).| <> 0 by A2, A14, Th4;

hence s . x <> 0 by A13, COMPLEX1:47; :: thesis: verum

then reconsider s = s as non-zero 0 -convergent Real_Sequence by A11, A12, FDIFF_1:def 1;

A15: J * I = id REAL by A1, A2, Lm1, FUNCT_1:39;

now :: thesis: for n being Element of NAT holds ||.((||.h.|| ") (#) (R1 /* h)).|| . n = |.((s ") (#) (R /* s)).| . n

then A23:
||.((||.h.|| ") (#) (R1 /* h)).|| = |.((s ") (#) (R /* s)).|
by FUNCT_2:63;reconsider f1 = R1 as Function ;

let n be Element of NAT ; :: thesis: ||.((||.h.|| ") (#) (R1 /* h)).|| . n = |.((s ") (#) (R /* s)).| . n

A16: rng h c= the carrier of (REAL-NS 1) ;

h . n in the carrier of (REAL-NS 1) ;

then A17: h . n in REAL 1 by REAL_NS1:def 4;

A18: (R0 * J) . (h . n) in REAL by XREAL_0:def 1;

R1 is total by A3;

then (R /* s) . n = R . (s . n) by FUNCT_2:115;

then (R /* s) . n = R . (J . (h . n)) by A5;

then (R /* s) . n = (J * I) . (R0 . (J . (h . n))) by A15;

then (R /* s) . n = (J * I) . ((R0 * J) . (h . n)) by A17, FUNCT_2:15;

then (R /* s) . n = J . (I . ((R0 * J) . (h . n))) by FUNCT_2:15, A18;

then A19: (R /* s) . n = J . ((I * (R0 * J)) . (h . n)) by A17, FUNCT_2:15;

NAT = dom h by FUNCT_2:def 1;

then A20: R1 . (h . n) = (f1 * h) . n by FUNCT_1:13;

dom R1 = REAL 1 by FUNCT_2:def 1;

then rng h c= dom R1 by A16, REAL_NS1:def 4;

then R1 . (h . n) = (R1 /* h) . n by A20, FUNCT_2:def 11;

then A21: (R /* s) . n = J . ((R1 /* h) . n) by A19, RELAT_1:36;

A22: s . n = J . (h . n) by A5;

||.((||.h.|| ") (#) (R1 /* h)).|| . n = ||.(((||.h.|| ") (#) (R1 /* h)) . n).|| by NORMSP_0:def 4

.= ||.(((||.h.|| ") . n) * ((R1 /* h) . n)).|| by NDIFF_1:def 2

.= |.((||.h.|| ") . n).| * ||.((R1 /* h) . n).|| by NORMSP_1:def 1

.= |.((||.h.|| . n) ").| * ||.((R1 /* h) . n).|| by VALUED_1:10

.= |.(||.(h . n).|| ").| * ||.((R1 /* h) . n).|| by NORMSP_0:def 4

.= (||.(h . n).|| ") * ||.((R1 /* h) . n).|| by ABSVALUE:def 1

.= (|.(s . n).| ") * ||.((R1 /* h) . n).|| by A2, A22, Th4

.= (|.(s . n).| ") * |.((R /* s) . n).| by A2, A21, Th4

.= (|.(s . n).| ") * (|.(R /* s).| . n) by SEQ_1:12

.= (((abs s) . n) ") * (|.(R /* s).| . n) by SEQ_1:12

.= (((abs s) ") . n) * (|.(R /* s).| . n) by VALUED_1:10

.= (((abs s) ") (#) |.(R /* s).|) . n by SEQ_1:8

.= (|.(s ").| (#) (abs (R /* s))) . n by SEQ_1:54 ;

hence ||.((||.h.|| ") (#) (R1 /* h)).|| . n = |.((s ") (#) (R /* s)).| . n by SEQ_1:52; :: thesis: verum

end;let n be Element of NAT ; :: thesis: ||.((||.h.|| ") (#) (R1 /* h)).|| . n = |.((s ") (#) (R /* s)).| . n

A16: rng h c= the carrier of (REAL-NS 1) ;

h . n in the carrier of (REAL-NS 1) ;

then A17: h . n in REAL 1 by REAL_NS1:def 4;

A18: (R0 * J) . (h . n) in REAL by XREAL_0:def 1;

R1 is total by A3;

then (R /* s) . n = R . (s . n) by FUNCT_2:115;

then (R /* s) . n = R . (J . (h . n)) by A5;

then (R /* s) . n = (J * I) . (R0 . (J . (h . n))) by A15;

then (R /* s) . n = (J * I) . ((R0 * J) . (h . n)) by A17, FUNCT_2:15;

then (R /* s) . n = J . (I . ((R0 * J) . (h . n))) by FUNCT_2:15, A18;

then A19: (R /* s) . n = J . ((I * (R0 * J)) . (h . n)) by A17, FUNCT_2:15;

NAT = dom h by FUNCT_2:def 1;

then A20: R1 . (h . n) = (f1 * h) . n by FUNCT_1:13;

dom R1 = REAL 1 by FUNCT_2:def 1;

then rng h c= dom R1 by A16, REAL_NS1:def 4;

then R1 . (h . n) = (R1 /* h) . n by A20, FUNCT_2:def 11;

then A21: (R /* s) . n = J . ((R1 /* h) . n) by A19, RELAT_1:36;

A22: s . n = J . (h . n) by A5;

||.((||.h.|| ") (#) (R1 /* h)).|| . n = ||.(((||.h.|| ") (#) (R1 /* h)) . n).|| by NORMSP_0:def 4

.= ||.(((||.h.|| ") . n) * ((R1 /* h) . n)).|| by NDIFF_1:def 2

.= |.((||.h.|| ") . n).| * ||.((R1 /* h) . n).|| by NORMSP_1:def 1

.= |.((||.h.|| . n) ").| * ||.((R1 /* h) . n).|| by VALUED_1:10

.= |.(||.(h . n).|| ").| * ||.((R1 /* h) . n).|| by NORMSP_0:def 4

.= (||.(h . n).|| ") * ||.((R1 /* h) . n).|| by ABSVALUE:def 1

.= (|.(s . n).| ") * ||.((R1 /* h) . n).|| by A2, A22, Th4

.= (|.(s . n).| ") * |.((R /* s) . n).| by A2, A21, Th4

.= (|.(s . n).| ") * (|.(R /* s).| . n) by SEQ_1:12

.= (((abs s) . n) ") * (|.(R /* s).| . n) by SEQ_1:12

.= (((abs s) ") . n) * (|.(R /* s).| . n) by VALUED_1:10

.= (((abs s) ") (#) |.(R /* s).|) . n by SEQ_1:8

.= (|.(s ").| (#) (abs (R /* s))) . n by SEQ_1:54 ;

hence ||.((||.h.|| ") (#) (R1 /* h)).|| . n = |.((s ") (#) (R /* s)).| . n by SEQ_1:52; :: thesis: verum

A24: lim ((s ") (#) (R /* s)) = 0 by FDIFF_1:def 2;

A25: (s ") (#) (R /* s) is convergent by FDIFF_1:def 2;

then lim |.((s ") (#) (R /* s)).| = |.(lim ((s ") (#) (R /* s))).| by SEQ_4:14;

then A26: lim |.((s ") (#) (R /* s)).| = 0 by A24, ABSVALUE:2;

A27: abs ((s ") (#) (R /* s)) is convergent by A25, SEQ_4:13;

A28: now :: thesis: for p being Real st 0 < p holds

ex m being Nat st

for n being Nat st m <= n holds

||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p

then
(||.h.|| ") (#) (R1 /* h) is convergent
by NORMSP_1:def 6;ex m being Nat st

for n being Nat st m <= n holds

||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p

let p be Real; :: thesis: ( 0 < p implies ex m being Nat st

for n being Nat st m <= n holds

||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p )

assume 0 < p ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p

then consider m being Nat such that

A29: for n being Nat st m <= n holds

|.((||.((||.h.|| ") (#) (R1 /* h)).|| . n) - 0).| < p by A23, A27, A26, SEQ_2:def 7;

reconsider m = m as Nat ;

take m = m; :: thesis: for n being Nat st m <= n holds

||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p

let n be Nat; :: thesis: ( m <= n implies ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p )

assume m <= n ; :: thesis: ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p

then |.((||.((||.h.|| ") (#) (R1 /* h)).|| . n) - 0).| < p by A29;

then A30: |.||.(((||.h.|| ") (#) (R1 /* h)) . n).||.| < p by NORMSP_0:def 4;

||.(((||.h.|| ") (#) (R1 /* h)) . n).|| < p by A30, ABSVALUE:def 1;

hence ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p by RLVECT_1:13; :: thesis: verum

end;for n being Nat st m <= n holds

||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p )

assume 0 < p ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p

then consider m being Nat such that

A29: for n being Nat st m <= n holds

|.((||.((||.h.|| ") (#) (R1 /* h)).|| . n) - 0).| < p by A23, A27, A26, SEQ_2:def 7;

reconsider m = m as Nat ;

take m = m; :: thesis: for n being Nat st m <= n holds

||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p

let n be Nat; :: thesis: ( m <= n implies ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p )

assume m <= n ; :: thesis: ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p

then |.((||.((||.h.|| ") (#) (R1 /* h)).|| . n) - 0).| < p by A29;

then A30: |.||.(((||.h.|| ") (#) (R1 /* h)) . n).||.| < p by NORMSP_0:def 4;

||.(((||.h.|| ") (#) (R1 /* h)) . n).|| < p by A30, ABSVALUE:def 1;

hence ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p by RLVECT_1:13; :: thesis: verum

hence ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS 1) ) by A28, NORMSP_1:def 7; :: thesis: verum

proof

let L be LinearFunc; :: thesis: (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1)

consider r being Real such that

A31: for p being Real holds L . p = r * p by FDIFF_1:def 3;

L is total by FDIFF_1:def 3;

then reconsider L0 = L as Function of REAL,REAL ;

reconsider r = r as Real ;

set K = |.r.|;

A32: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

(I * L0) * J is Function of (REAL 1),(REAL 1) ;

then reconsider L1 = (I * L) * J as Function of (REAL-NS 1),(REAL-NS 1) by A32;

A33: dom L1 = REAL 1 by A32, FUNCT_2:def 1;

A34: dom L0 = REAL by FUNCT_2:def 1;

hence (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by A43, LOPBAN_1:def 8; :: thesis: verum

end;consider r being Real such that

A31: for p being Real holds L . p = r * p by FDIFF_1:def 3;

L is total by FDIFF_1:def 3;

then reconsider L0 = L as Function of REAL,REAL ;

reconsider r = r as Real ;

set K = |.r.|;

A32: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

(I * L0) * J is Function of (REAL 1),(REAL 1) ;

then reconsider L1 = (I * L) * J as Function of (REAL-NS 1),(REAL-NS 1) by A32;

A33: dom L1 = REAL 1 by A32, FUNCT_2:def 1;

A34: dom L0 = REAL by FUNCT_2:def 1;

A35: now :: thesis: for x, y being VECTOR of (REAL-NS 1) holds L1 . (x + y) = (L1 . x) + (L1 . y)

let x, y be VECTOR of (REAL-NS 1); :: thesis: L1 . (x + y) = (L1 . x) + (L1 . y)

A36: (J . x) + (J . y) in REAL by XREAL_0:def 1;

A37: J . x in REAL by XREAL_0:def 1;

J . y in REAL by XREAL_0:def 1;

then I . (L . (J . y)) = (I * L) . (J . y) by A34, FUNCT_1:13;

then A38: I . (L . (J . y)) = L1 . y by A32, A33, FUNCT_1:12;

L1 . (x + y) = (I * L) . (J . (x + y)) by A32, A33, FUNCT_1:12;

then L1 . (x + y) = (I * L) . ((J . x) + (J . y)) by A2, Th4;

then L1 . (x + y) = I . (L . ((J . x) + (J . y))) by A36, A34, FUNCT_1:13;

then L1 . (x + y) = I . (r * ((J . x) + (J . y))) by A31;

then L1 . (x + y) = I . ((r * (J . x)) + (r * (J . y))) ;

then L1 . (x + y) = I . ((L . (J . x)) + (r * (J . y))) by A31;

then A39: L1 . (x + y) = I . ((L . (J . x)) + (L . (J . y))) by A31;

I . (L . (J . x)) = (I * L) . (J . x) by A37, A34, FUNCT_1:13;

then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:12;

hence L1 . (x + y) = (L1 . x) + (L1 . y) by A1, A38, A39, Th3; :: thesis: verum

end;A36: (J . x) + (J . y) in REAL by XREAL_0:def 1;

A37: J . x in REAL by XREAL_0:def 1;

J . y in REAL by XREAL_0:def 1;

then I . (L . (J . y)) = (I * L) . (J . y) by A34, FUNCT_1:13;

then A38: I . (L . (J . y)) = L1 . y by A32, A33, FUNCT_1:12;

L1 . (x + y) = (I * L) . (J . (x + y)) by A32, A33, FUNCT_1:12;

then L1 . (x + y) = (I * L) . ((J . x) + (J . y)) by A2, Th4;

then L1 . (x + y) = I . (L . ((J . x) + (J . y))) by A36, A34, FUNCT_1:13;

then L1 . (x + y) = I . (r * ((J . x) + (J . y))) by A31;

then L1 . (x + y) = I . ((r * (J . x)) + (r * (J . y))) ;

then L1 . (x + y) = I . ((L . (J . x)) + (r * (J . y))) by A31;

then A39: L1 . (x + y) = I . ((L . (J . x)) + (L . (J . y))) by A31;

I . (L . (J . x)) = (I * L) . (J . x) by A37, A34, FUNCT_1:13;

then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:12;

hence L1 . (x + y) = (L1 . x) + (L1 . y) by A1, A38, A39, Th3; :: thesis: verum

now :: thesis: for x being VECTOR of (REAL-NS 1)

for a being Real holds L1 . (a * x) = a * (L1 . x)

then reconsider L1 = L1 as LinearOperator of (REAL-NS 1),(REAL-NS 1) by A35, VECTSP_1:def 20, LOPBAN_1:def 5;for a being Real holds L1 . (a * x) = a * (L1 . x)

let x be VECTOR of (REAL-NS 1); :: thesis: for a being Real holds L1 . (a * x) = a * (L1 . x)

let a be Real; :: thesis: L1 . (a * x) = a * (L1 . x)

reconsider aa = a as Real ;

A40: J . x in REAL by XREAL_0:def 1;

A41: aa * (J . x) in REAL by XREAL_0:def 1;

L1 . (a * x) = (I * L) . (J . (a * x)) by A32, A33, FUNCT_1:12;

then L1 . (a * x) = (I * L) . (a * (J . x)) by A2, Th4;

then L1 . (aa * x) = I . (L . (aa * (J . x))) by A41, A34, FUNCT_1:13;

then L1 . (a * x) = I . (r * (a * (J . x))) by A31;

then L1 . (a * x) = I . (a * (r * (J . x))) ;

then A42: L1 . (a * x) = I . (a * (L . (J . x))) by A31;

I . (L . (J . x)) = (I * L) . (J . x) by A40, A34, FUNCT_1:13;

then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:12;

hence L1 . (a * x) = a * (L1 . x) by A1, A42, Th3; :: thesis: verum

end;let a be Real; :: thesis: L1 . (a * x) = a * (L1 . x)

reconsider aa = a as Real ;

A40: J . x in REAL by XREAL_0:def 1;

A41: aa * (J . x) in REAL by XREAL_0:def 1;

L1 . (a * x) = (I * L) . (J . (a * x)) by A32, A33, FUNCT_1:12;

then L1 . (a * x) = (I * L) . (a * (J . x)) by A2, Th4;

then L1 . (aa * x) = I . (L . (aa * (J . x))) by A41, A34, FUNCT_1:13;

then L1 . (a * x) = I . (r * (a * (J . x))) by A31;

then L1 . (a * x) = I . (a * (r * (J . x))) ;

then A42: L1 . (a * x) = I . (a * (L . (J . x))) by A31;

I . (L . (J . x)) = (I * L) . (J . x) by A40, A34, FUNCT_1:13;

then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:12;

hence L1 . (a * x) = a * (L1 . x) by A1, A42, Th3; :: thesis: verum

A43: now :: thesis: for x being VECTOR of (REAL-NS 1) holds ||.(L1 . x).|| <= |.r.| * ||.x.||

0 <= |.r.|
by COMPLEX1:46;let x be VECTOR of (REAL-NS 1); :: thesis: ||.(L1 . x).|| <= |.r.| * ||.x.||

J . x in REAL by XREAL_0:def 1;

then I . (L . (J . x)) = (I * L) . (J . x) by A34, FUNCT_1:13;

then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:12;

then ||.(L1 . x).|| = |.(L . (J . x)).| by A1, Th3;

then ||.(L1 . x).|| = |.(r * (J . x)).| by A31;

then ||.(L1 . x).|| = |.r.| * |.(J . x).| by COMPLEX1:65;

hence ||.(L1 . x).|| <= |.r.| * ||.x.|| by A2, Th4; :: thesis: verum

end;J . x in REAL by XREAL_0:def 1;

then I . (L . (J . x)) = (I * L) . (J . x) by A34, FUNCT_1:13;

then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:12;

then ||.(L1 . x).|| = |.(L . (J . x)).| by A1, Th3;

then ||.(L1 . x).|| = |.(r * (J . x)).| by A31;

then ||.(L1 . x).|| = |.r.| * |.(J . x).| by COMPLEX1:65;

hence ||.(L1 . x).|| <= |.r.| * ||.x.|| by A2, Th4; :: thesis: verum

hence (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by A43, LOPBAN_1:def 8; :: thesis: verum