let Y be RealNormSpace; :: thesis: for I being Function of REAL,()
for x0 being Point of ()
for y0 being Element of REAL
for g being PartFunc of REAL,Y
for f being PartFunc of (),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let I be Function of REAL,(); :: thesis: for x0 being Point of ()
for y0 being Element of REAL
for g being PartFunc of REAL,Y
for f being PartFunc of (),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let x0 be Point of (); :: thesis: for y0 being Element of REAL
for g being PartFunc of REAL,Y
for f being PartFunc of (),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let y0 be Element of REAL ; :: thesis: for g being PartFunc of REAL,Y
for f being PartFunc of (),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let g be PartFunc of REAL,Y; :: thesis: for f being PartFunc of (),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

let f be PartFunc of (),Y; :: thesis: ( I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 implies ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) )
assume that
A1: I = (proj (1,1)) " and
A2: x0 in dom f and
A3: y0 in dom g and
A4: x0 = <*y0*> and
A5: f * I = g and
A6: f is_differentiable_in x0 ; :: thesis: ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
reconsider J = proj (1,1) as Function of (),REAL by Lm1;
consider NN being Neighbourhood of x0 such that
A7: NN c= dom f and
A8: ex L being Point of () ex R being RestFunc of (),Y st
for x being Point of () st x in NN holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A6;
A9: I * J = id () by ;
A10: g * J = f * (id ()) by
.= f by FUNCT_2:17 ;
consider e being Real such that
A11: 0 < e and
A12: { z where z is Point of () : ||.(z - x0).|| < e } c= NN by NFCONT_1:def 1;
consider L being Point of (), R being RestFunc of (),Y such that
A13: for x9 being Point of () st x9 in NN holds
(f /. x9) - (f /. x0) = (L . (x9 - x0)) + (R /. (x9 - x0)) by A8;
reconsider R0 = R * I as RestFunc of Y by ;
L is LinearOperator of (),Y by LOPBAN_1:def 9;
then reconsider L0 = L * I as LinearFunc of Y by ;
set N = { z where z is Point of () : ||.(z - x0).|| < e } ;
A14: { z where z is Point of () : ||.(z - x0).|| < e } c= the carrier of ()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { z where z is Point of () : ||.(z - x0).|| < e } or y in the carrier of () )
assume y in { z where z is Point of () : ||.(z - x0).|| < e } ; :: thesis: y in the carrier of ()
then ex z being Point of () st
( y = z & ||.(z - x0).|| < e ) ;
hence y in the carrier of () ; :: thesis: verum
end;
then reconsider N = { z where z is Point of () : ||.(z - x0).|| < e } as Neighbourhood of x0 by ;
set N0 = { z where z is Element of REAL : |.(z - y0).| < e } ;
now :: thesis: for z being object holds
( ( z in { z where z is Element of REAL : |.(z - y0).| < e } implies z in J .: N ) & ( z in J .: N implies z in { z where z is Element of REAL : |.(z - y0).| < e } ) )
let z be object ; :: thesis: ( ( z in { z where z is Element of REAL : |.(z - y0).| < e } implies z in J .: N ) & ( z in J .: N implies z in { z where z is Element of REAL : |.(z - y0).| < e } ) )
hereby :: thesis: ( z in J .: N implies z in { z where z is Element of REAL : |.(z - y0).| < e } )
assume z in { z where z is Element of REAL : |.(z - y0).| < e } ; :: thesis: z in J .: N
then consider y9 being Element of REAL such that
A16: z = y9 and
A17: |.(y9 - y0).| < e ;
reconsider w = I . y9 as Point of () ;
x0 = I . y0 by A1, A4, Lm2;
then w - x0 = I . (y9 - y0) by ;
then ||.(w - x0).|| = |.(y9 - y0).| by ;
then A18: w in { z0 where z0 is Point of () : ||.(z0 - x0).|| < e } by A17;
J . (I . y9) = y9 by ;
hence z in J .: N by ; :: thesis: verum
end;
assume z in J .: N ; :: thesis: z in { z where z is Element of REAL : |.(z - y0).| < e }
then consider ww being object such that
A19: ( ww in REAL 1 & ww in N & z = J . ww ) by FUNCT_2:64;
consider w being Point of () such that
A21: ( ww = w & ||.(w - x0).|| < e ) by A19;
reconsider y9 = J . w as Element of REAL ;
J . x0 = y0 by ;
then J . (w - x0) = y9 - y0 by PDIFF_1:4;
then |.(y9 - y0).| < e by ;
hence z in { z where z is Element of REAL : |.(z - y0).| < e } by ; :: thesis: verum
end;
then A23: { z where z is Element of REAL : |.(z - y0).| < e } = J .: N by TARSKI:2;
J .: (dom f) = J .: (J " (dom g)) by ;
then A24: J .: (dom f) = dom (f * I) by ;
A25: I * J = id (REAL 1) by ;
A261: N c= dom f by ;
then A26: { z where z is Element of REAL : |.(z - y0).| < e } c= dom (f * I) by ;
A27: ].(y0 - e),(y0 + e).[ c= { z where z is Element of REAL : |.(z - y0).| < e }
proof
now :: thesis: for d being object st d in ].(y0 - e),(y0 + e).[ holds
d in { z where z is Element of REAL : |.(z - y0).| < e }
let d be object ; :: thesis: ( d in ].(y0 - e),(y0 + e).[ implies d in { z where z is Element of REAL : |.(z - y0).| < e } )
assume A28: d in ].(y0 - e),(y0 + e).[ ; :: thesis: d in { z where z is Element of REAL : |.(z - y0).| < e }
then reconsider y1 = d as Element of REAL ;
|.(y1 - y0).| < e by ;
hence d in { z where z is Element of REAL : |.(z - y0).| < e } ; :: thesis: verum
end;
hence ].(y0 - e),(y0 + e).[ c= { z where z is Element of REAL : |.(z - y0).| < e } ; :: thesis: verum
end;
{ z where z is Element of REAL : |.(z - y0).| < e } c= ].(y0 - e),(y0 + e).[
proof
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in { z where z is Element of REAL : |.(z - y0).| < e } or d in ].(y0 - e),(y0 + e).[ )
assume d in { z where z is Element of REAL : |.(z - y0).| < e } ; :: thesis: d in ].(y0 - e),(y0 + e).[
then ex r being Element of REAL st
( d = r & |.(r - y0).| < e ) ;
hence d in ].(y0 - e),(y0 + e).[ by RCOMP_1:1; :: thesis: verum
end;
then { z where z is Element of REAL : |.(z - y0).| < e } = ].(y0 - e),(y0 + e).[ by ;
then A29: { z where z is Element of REAL : |.(z - y0).| < e } is Neighbourhood of y0 by ;
N c= REAL 1 by ;
then (I * J) .: N = N by ;
then A30: I .: { z where z is Element of REAL : |.(z - y0).| < e } = N by ;
A31: for y1 being Real st y1 in { z where z is Element of REAL : |.(z - y0).| < e } holds
((f * I) /. y1) - ((f * I) /. y0) = (L0 /. (y1 - y0)) + (R0 /. (y1 - y0))
proof
let y1 be Real; :: thesis: ( y1 in { z where z is Element of REAL : |.(z - y0).| < e } implies ((f * I) /. y1) - ((f * I) /. y0) = (L0 /. (y1 - y0)) + (R0 /. (y1 - y0)) )
reconsider yy = y1 as Element of REAL by XREAL_0:def 1;
reconsider y9 = I . yy as Point of () ;
R is total by NDIFF_1:def 5;
then A32: dom R = the carrier of () by PARTFUN1:def 2;
R0 is total by NDIFF_3:def 1;
then A33: dom (R * I) = REAL by PARTFUN1:def 2;
reconsider dy1y0 = y1 - y0 as Element of REAL by XREAL_0:def 1;
I . dy1y0 in dom R by A32;
then R /. (I . (y1 - y0)) = R . (I . (y1 - y0)) by PARTFUN1:def 6;
then R /. (I . dy1y0) = R0 . dy1y0 by ;
then A34: R /. (I . (y1 - y0)) = R0 /. dy1y0 by ;
L0 is total ;
then A35: dom (L * I) = REAL by PARTFUN1:def 2;
assume A36: y1 in { z where z is Element of REAL : |.(z - y0).| < e } ; :: thesis: ((f * I) /. y1) - ((f * I) /. y0) = (L0 /. (y1 - y0)) + (R0 /. (y1 - y0))
then A37: I . yy in N by ;
then f /. (I . y1) = f . (I . y1) by ;
then f /. (I . y1) = (f * I) . y1 by ;
then A39: f /. (I . y1) = (f * I) /. y1 by ;
A40: x0 = I . y0 by A4, A1, Lm2;
then f /. (I . y0) = f . (I . y0) by ;
then f /. (I . y0) = (f * I) . y0 by ;
then A41: f /. (I . y0) = (f * I) /. y0 by ;
reconsider d = y1 - y0 as Element of REAL by XREAL_0:def 1;
(f /. y9) - (f /. x0) = (L . (y9 - x0)) + (R /. (y9 - x0)) by ;
then A42: (f /. (I . y1)) - (f /. (I . y0)) = (L . (I . d)) + (R /. (y9 - x0)) by ;
L . (I . d) = L0 /. dy1y0 by ;
hence ((f * I) /. y1) - ((f * I) /. y0) = (L0 /. (y1 - y0)) + (R0 /. (y1 - y0)) by ; :: thesis: verum
end;
hence g is_differentiable_in y0 by ; :: thesis: ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )
then diff ((f * I),y0) = L0 /. jj by ;
hence A45: diff (g,y0) = ((diff (f,x0)) * I) . 1 by
.= (diff (f,x0)) . (I . jj) by
.= (diff (f,x0)) . <*1*> by ;
:: thesis: for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0))
let r be Element of REAL ; :: thesis: (diff (f,x0)) . <*r*> = r * (diff (g,y0))
A46: <*jj*> is Element of REAL 1 by FINSEQ_2:98;
then reconsider x = <*1*> as Point of () by REAL_NS1:def 4;
A47: diff (f,x0) is LinearOperator of (),Y by LOPBAN_1:def 9;
thus (diff (f,x0)) . <*r*> = (diff (f,x0)) . <*(r * 1)*>
.= (diff (f,x0)) . (r * <*1*>) by RVSUM_1:47
.= (diff (f,x0)) . (r * x) by
.= r * (diff (g,y0)) by ; :: thesis: verum