let Y be RealNormSpace; :: thesis: for J being Function of (REAL-NS 1),REAL st J = proj (1,1) holds

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

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

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

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

consider r being Point of Y such that

A27: for p being Real holds L /. p = p * r by NDIFF_3:def 2;

reconsider L0 = L as Function of REAL,Y ;

set K = ||.r.||;

reconsider L1 = L * J as Function of (REAL-NS 1),Y ;

A28: dom L1 = REAL 1 by Lm1, FUNCT_2:def 1;

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

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

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

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

proof

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

A2: R is total by NDIFF_3:def 1;

reconsider R0 = R as Function of REAL,Y by A2;

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

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

( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. Y )

end;A2: R is total by NDIFF_3:def 1;

reconsider R0 = R as Function of REAL,Y by A2;

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

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

( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. Y )

proof

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

assume A3: h is non-zero ; :: thesis: ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. Y )

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

deffunc H_{1}( Nat) -> Element of REAL = 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 A11: lim s = 0 by A7, SEQ_2:def 7;

( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. Y ) by NDIFF_3:def 1;

then A22: lim ||.((s ") (#) (R /* s)).|| = ||.(0. Y).|| by LOPBAN_1:20;

A23: ||.((s ") (#) (R /* s)).|| is convergent by NDIFF_3:def 1, NORMSP_1:23;

hence ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. Y ) by A24, NORMSP_1:def 7; :: thesis: verum

end;assume A3: h is non-zero ; :: thesis: ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. Y )

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
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;

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;

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 m <= n ; :: thesis: |.((s . n) - 0).| < p

then A91: ||.((h . n) - (0. (REAL-NS 1))).|| < p by A8;

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

hence |.((s . n) - 0).| < p by A1, A91, PDIFF_1:4; :: thesis: verum

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

then A91: ||.((h . n) - (0. (REAL-NS 1))).|| < p by A8;

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

hence |.((s . n) - 0).| < p by A1, A91, PDIFF_1:4; :: thesis: verum

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

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

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

s . x <> 0

then reconsider s = s as non-zero 0 -convergent Real_Sequence by A7, SEQ_2:def 6, A11, FDIFF_1:def 1, 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: ||.(h . n).|| <> 0 by NORMSP_0:def 5, A3, NDIFF_1:6;

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

then |.(s . n).| <> 0 by A1, A13, PDIFF_1:4;

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

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

then reconsider n = x as Element of NAT ;

A13: ||.(h . n).|| <> 0 by NORMSP_0:def 5, A3, NDIFF_1:6;

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

then |.(s . n).| <> 0 by A1, A13, PDIFF_1:4;

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

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

then A19:
||.((||.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

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

then A14: rng h c= dom R1 by FUNCT_2:def 1;

(R /* s) . n = R . (s . n) by NDIFF_3:def 1, FUNCT_2:115;

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

NAT = dom h by FUNCT_2:def 1;

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

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

A18: 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 A1, A18, PDIFF_1:4

.= (|.(s . n).| ") * ||.((R /* s) . n).|| by A17, A15, FUNCT_2:15

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

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

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

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

.= ||.(((s ") . n) * ((R /* s) . n)).|| by NORMSP_1:def 1

.= ||.(((s ") (#) (R /* s)) . n).|| by NDIFF_1:def 2

.= ||.((s ") (#) (R /* s)).|| . n by NORMSP_0:def 4 ;

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

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

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

then A14: rng h c= dom R1 by FUNCT_2:def 1;

(R /* s) . n = R . (s . n) by NDIFF_3:def 1, FUNCT_2:115;

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

NAT = dom h by FUNCT_2:def 1;

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

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

A18: 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 A1, A18, PDIFF_1:4

.= (|.(s . n).| ") * ||.((R /* s) . n).|| by A17, A15, FUNCT_2:15

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

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

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

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

.= ||.(((s ") . n) * ((R /* s) . n)).|| by NORMSP_1:def 1

.= ||.(((s ") (#) (R /* s)) . n).|| by NDIFF_1:def 2

.= ||.((s ") (#) (R /* s)).|| . n by NORMSP_0:def 4 ;

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

( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. Y ) by NDIFF_3:def 1;

then A22: lim ||.((s ") (#) (R /* s)).|| = ||.(0. Y).|| by LOPBAN_1:20;

A23: ||.((s ") (#) (R /* s)).|| is convergent by NDIFF_3:def 1, NORMSP_1:23;

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

ex n0 being Nat st

for m being Nat st n0 <= m holds

||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p

then
(||.h.|| ") (#) (R1 /* h) is convergent
;ex n0 being Nat st

for m being Nat st n0 <= m holds

||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p

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

for m being Nat st n0 <= m holds

||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p )

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

for m being Nat st n0 <= m holds

||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p

then consider n0 being Nat such that

A25: for m being Nat st n0 <= m holds

|.((||.((||.h.|| ") (#) (R1 /* h)).|| . m) - 0).| < p by A19, A23, A22, SEQ_2:def 7;

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

||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p

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

||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p )

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

for m being Nat st n0 <= m holds

||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p

then consider n0 being Nat such that

A25: for m being Nat st n0 <= m holds

|.((||.((||.h.|| ") (#) (R1 /* h)).|| . m) - 0).| < p by A19, A23, A22, SEQ_2:def 7;

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

||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p

hereby :: thesis: verum

let m be Nat; :: thesis: ( n0 <= m implies ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p )

assume n0 <= m ; :: thesis: ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p

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

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

hence ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p by ABSVALUE:def 1; :: thesis: verum

end;assume n0 <= m ; :: thesis: ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p

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

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

hence ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. Y)).|| < p by ABSVALUE:def 1; :: thesis: verum

hence ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. Y ) by A24, NORMSP_1:def 7; :: thesis: verum

consider r being Point of Y such that

A27: for p being Real holds L /. p = p * r by NDIFF_3:def 2;

reconsider L0 = L as Function of REAL,Y ;

set K = ||.r.||;

reconsider L1 = L * J as Function of (REAL-NS 1),Y ;

A28: dom L1 = REAL 1 by Lm1, FUNCT_2:def 1;

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

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

L1 . (x + y) = L /. (J . (x + y)) by Lm1, A28, FUNCT_1:12;

then L1 . (x + y) = L /. ((J . x) + (J . y)) by A1, PDIFF_1:4;

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

then L1 . (x + y) = ((J . x) * r) + ((J . y) * r) by RLVECT_1:def 6;

then L1 . (x + y) = (L /. (J . x)) + ((J . y) * r) by A27;

then A30: L1 . (x + y) = (L /. (J . x)) + (L /. (J . y)) by A27;

L /. (J . x) = L1 . x by Lm1, A28, FUNCT_1:12;

hence L1 . (x + y) = (L1 . x) + (L1 . y) by Lm1, A28, A30, FUNCT_1:12; :: thesis: verum

end;L1 . (x + y) = L /. (J . (x + y)) by Lm1, A28, FUNCT_1:12;

then L1 . (x + y) = L /. ((J . x) + (J . y)) by A1, PDIFF_1:4;

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

then L1 . (x + y) = ((J . x) * r) + ((J . y) * r) by RLVECT_1:def 6;

then L1 . (x + y) = (L /. (J . x)) + ((J . y) * r) by A27;

then A30: L1 . (x + y) = (L /. (J . x)) + (L /. (J . y)) by A27;

L /. (J . x) = L1 . x by Lm1, A28, FUNCT_1:12;

hence L1 . (x + y) = (L1 . x) + (L1 . y) by Lm1, A28, A30, FUNCT_1:12; :: thesis: verum

now :: thesis: for x being Point 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),Y by A29, LOPBAN_1:def 5, VECTSP_1:def 20;for a being Real holds L1 . (a * x) = a * (L1 . x)

let x be Point 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)

L1 . (a * x) = L /. (J . (a * x)) by Lm1, A28, FUNCT_1:12;

then L1 . (a * x) = L /. (a * (J . x)) by A1, PDIFF_1:4;

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

then A31: L1 . (a * x) = a * ((J . x) * r) by RLVECT_1:def 7;

L /. (J . x) = L1 . x by Lm1, A28, FUNCT_1:12;

hence L1 . (a * x) = a * (L1 . x) by A31, A27; :: thesis: verum

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

L1 . (a * x) = L /. (J . (a * x)) by Lm1, A28, FUNCT_1:12;

then L1 . (a * x) = L /. (a * (J . x)) by A1, PDIFF_1:4;

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

then A31: L1 . (a * x) = a * ((J . x) * r) by RLVECT_1:def 7;

L /. (J . x) = L1 . x by Lm1, A28, FUNCT_1:12;

hence L1 . (a * x) = a * (L1 . x) by A31, A27; :: thesis: verum

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

hence
L * J is Lipschitzian LinearOperator of (REAL-NS 1),Y
by LOPBAN_1:def 8; :: thesis: verumlet x be Point of (REAL-NS 1); :: thesis: ||.(L1 . x).|| <= ||.r.|| * ||.x.||

||.(L1 . x).|| = ||.(L /. (J . x)).|| by Lm1, A28, FUNCT_1:12;

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

then ||.(L1 . x).|| = ||.r.|| * |.(J . x).| by NORMSP_1:def 1;

hence ||.(L1 . x).|| <= ||.r.|| * ||.x.|| by A1, PDIFF_1:4; :: thesis: verum

end;||.(L1 . x).|| = ||.(L /. (J . x)).|| by Lm1, A28, FUNCT_1:12;

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

then ||.(L1 . x).|| = ||.r.|| * |.(J . x).| by NORMSP_1:def 1;

hence ||.(L1 . x).|| <= ||.r.|| * ||.x.|| by A1, PDIFF_1:4; :: thesis: verum