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

let J be Function of (),REAL; :: thesis: ( J = proj (1,1) implies ( ( for R being RestFunc of Y holds R * J is RestFunc of (),Y ) & ( for L being LinearFunc of Y holds L * J is Lipschitzian LinearOperator of (),Y ) ) )
assume A1: J = proj (1,1) ; :: thesis: ( ( for R being RestFunc of Y holds R * J is RestFunc of (),Y ) & ( for L being LinearFunc of Y holds L * J is Lipschitzian LinearOperator of (),Y ) )
thus for R being RestFunc of Y holds R * J is RestFunc of (),Y :: thesis: for L being LinearFunc of Y holds L * J is Lipschitzian LinearOperator of (),Y
proof
let R be RestFunc of Y; :: thesis: R * J is RestFunc of (),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 (),Y ;
for h being 0. () -convergent sequence of () st h is non-zero holds
( () (#) (R1 /* h) is convergent & lim (() (#) (R1 /* h)) = 0. Y )
proof
let h be 0. () -convergent sequence of (); :: thesis: ( h is non-zero implies ( () (#) (R1 /* h) is convergent & lim (() (#) (R1 /* h)) = 0. Y ) )
assume A3: h is non-zero ; :: thesis: ( () (#) (R1 /* h) is convergent & lim (() (#) (R1 /* h)) = 0. Y )
A4: lim h = 0. () by NDIFF_1:def 4;
deffunc H1( Nat) -> Element of REAL = J . (h . \$1);
consider s being Real_Sequence such that
A5: for n being Nat holds s . n = H1(n) from SEQ_1:sch 1();
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
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. ())).|| < p by ;
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
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. ())).|| < p by A8;
s . n = J . (h . n) by A5;
hence |.((s . n) - 0).| < p by ; :: thesis: verum
end;
hence for n being Nat st m <= n holds
|.((s . n) - 0).| < p ; :: thesis: verum
end;
then s is convergent by SEQ_2:def 6;
then A11: lim s = 0 by ;
now :: thesis: for x being object st x in NAT holds
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 ;
s . n = J . (h . n) by A5;
then |.(s . n).| <> 0 by ;
hence s . x <> 0 by COMPLEX1:47; :: thesis: verum
end;
then reconsider s = s as non-zero 0 -convergent Real_Sequence by ;
now :: thesis: for n being Element of NAT holds ||.(() (#) (R1 /* h)).|| . n = ||.((s ") (#) (R /* s)).|| . n
reconsider f1 = R1 as Function ;
let n be Element of NAT ; :: thesis: ||.(() (#) (R1 /* h)).|| . n = ||.((s ") (#) (R /* s)).|| . n
rng h c= the carrier of () ;
then A14: rng h c= dom R1 by FUNCT_2:def 1;
(R /* s) . n = R . (s . n) by ;
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 ;
A18: s . n = J . (h . n) by A5;
||.(() (#) (R1 /* h)).|| . n = ||.((() (#) (R1 /* h)) . n).|| by NORMSP_0:def 4
.= ||.((() . n) * ((R1 /* h) . n)).|| by NDIFF_1:def 2
.= |.(() . n).| * ||.((R1 /* h) . n).|| by NORMSP_1:def 1
.= |.(( . 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
.= (|.(s . n).| ") * ||.((R /* s) . n).|| by
.= (((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 ||.(() (#) (R1 /* h)).|| . n = ||.((s ") (#) (R /* s)).|| . n ; :: thesis: verum
end;
then A19: ||.(() (#) (R1 /* h)).|| = ||.((s ") (#) (R /* s)).|| by FUNCT_2:63;
( (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 ;
A24: now :: thesis: for p being Real st 0 < p holds
ex n0 being Nat st
for m being Nat st n0 <= m holds
||.(((() (#) (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
||.(((() (#) (R1 /* h)) . m) - (0. Y)).|| < p )

assume 0 < p ; :: thesis: ex n0 being Nat st
for m being Nat st n0 <= m holds
||.(((() (#) (R1 /* h)) . m) - (0. Y)).|| < p

then consider n0 being Nat such that
A25: for m being Nat st n0 <= m holds
|.((||.(() (#) (R1 /* h)).|| . m) - 0).| < p by ;
take n0 = n0; :: thesis: for m being Nat st n0 <= m holds
||.(((() (#) (R1 /* h)) . m) - (0. Y)).|| < p

hereby :: thesis: verum
let m be Nat; :: thesis: ( n0 <= m implies ||.(((() (#) (R1 /* h)) . m) - (0. Y)).|| < p )
assume n0 <= m ; :: thesis: ||.(((() (#) (R1 /* h)) . m) - (0. Y)).|| < p
then |.((||.(() (#) (R1 /* h)).|| . m) - 0).| < p by A25;
then |.||.((() (#) (R1 /* h)) . m).||.| < p by NORMSP_0:def 4;
hence ||.(((() (#) (R1 /* h)) . m) - (0. Y)).|| < p by ABSVALUE:def 1; :: thesis: verum
end;
end;
then (||.h.|| ") (#) (R1 /* h) is convergent ;
hence ( (||.h.|| ") (#) (R1 /* h) is convergent & lim (() (#) (R1 /* h)) = 0. Y ) by ; :: thesis: verum
end;
hence R * J is RestFunc of (),Y by NDIFF_1:def 5; :: thesis: verum
end;
let L be LinearFunc of Y; :: thesis: L * J is Lipschitzian LinearOperator of (),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 = ;
reconsider L1 = L * J as Function of (),Y ;
A28: dom L1 = REAL 1 by ;
A29: now :: thesis: for x, y being Point of () holds L1 . (x + y) = (L1 . x) + (L1 . y)
let x, y be Point of (); :: thesis: L1 . (x + y) = (L1 . x) + (L1 . y)
L1 . (x + y) = L /. (J . (x + y)) by ;
then L1 . (x + y) = L /. ((J . x) + (J . y)) by ;
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 ;
hence L1 . (x + y) = (L1 . x) + (L1 . y) by ; :: thesis: verum
end;
now :: thesis: for x being Point of ()
for a being Real holds L1 . (a * x) = a * (L1 . x)
let x be Point of (); :: 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 ;
then L1 . (a * x) = L /. (a * (J . x)) by ;
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 ;
hence L1 . (a * x) = a * (L1 . x) by ; :: thesis: verum
end;
then reconsider L1 = L1 as LinearOperator of (),Y by ;
now :: thesis: for x being Point of () holds ||.(L1 . x).|| <= *
let x be Point of (); :: thesis: ||.(L1 . x).|| <= *
||.(L1 . x).|| = ||.(L /. (J . x)).|| by ;
then ||.(L1 . x).|| = ||.((J . x) * r).|| by A27;
then ||.(L1 . x).|| = * |.(J . x).| by NORMSP_1:def 1;
hence ||.(L1 . x).|| <= * by ; :: thesis: verum
end;
hence L * J is Lipschitzian LinearOperator of (),Y by LOPBAN_1:def 8; :: thesis: verum