let Y be RealNormSpace; :: thesis:
let I be Function of REAL,(REAL-NS 1); :: thesis:
let x0 be Point of (REAL-NS 1); :: thesis:
let y0 be Element of REAL ; :: thesis:
let g be PartFunc of REAL,Y; :: thesis:
let f be PartFunc of (REAL-NS 1),Y; :: thesis:
assume A1: ( I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 ) ; :: thesis:
reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;
reconsider j1 = 1 as Real ;
<*jj*> in REAL 1 by FINSEQ_2:98;
then reconsider t = <*jj*> as Point of (REAL-NS 1) by REAL_NS1:def 4;
J . t = jj by Lm2;
then ||.t.|| = |.j1.| by PDIFF_1:4;
then A3: ||.t.|| = 1 by ABSVALUE:def 1;
reconsider dfx0 = diff (f,x0) as Lipschitzian LinearOperator of (REAL-NS 1),Y by LOPBAN_1:def 9;
set A = PreNorms dfx0;
||.(diff (g,y0)).|| = ||.((diff (f,x0)) . t).|| by A1, FTh42;
then A5: ||.(diff (g,y0)).|| in PreNorms dfx0 by A3;
A6: ||.(diff (f,x0)).|| = upper_bound (PreNorms (modetrans ((diff (f,x0)),(REAL-NS 1),Y))) by LOPBAN_1:def 13
.= upper_bound (PreNorms dfx0) by LOPBAN_1:29 ;
PreNorms dfx0 is bounded_above by LOPBAN_1:27;
then A7: ||.(diff (g,y0)).|| <= ||.(diff (f,x0)).|| by A6, A5, SEQ_4:def 1;
for r being Real st r in PreNorms dfx0 holds
r <= ||.(diff (g,y0)).||

proof

let r be Real; :: thesis:
assume r in PreNorms dfx0 ; :: thesis:
then consider v being VECTOR of (REAL-NS 1) such that
A8: ( r = ||.(dfx0 . v).|| & ||.v.|| <= 1 ) ;
consider s being Real such that
X12: v = <*s*> by LM519A;
reconsider J = proj (1,1) as Function of (REAL 1),REAL ;
J . v = s by X12, PDIFF_1:1;
then X13: ||.v.|| = |.s.| by PDIFF_1:4;
reconsider s1 = s as Element of REAL by XREAL_0:def 1;
A9: (diff (f,x0)) . <*s1*> = s1 * (diff (g,y0)) by A1, FTh42;
|.s.| * ||.(diff (g,y0)).|| <= 1 * ||.(diff (g,y0)).|| by A8, X13, XREAL_1:64;
hence r <= ||.(diff (g,y0)).|| by A8, A9, X12, NORMSP_1:def 1; :: thesis:

end;

then ||.(diff (f,x0)).|| <= ||.(diff (g,y0)).|| by A6, SEQ_4:45;
hence ||.(diff (g,y0)).|| = ||.(diff (f,x0)).|| by A7, XXREAL_0:1; :: thesis: