let n be non zero Element of NAT ; :: thesis: for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) 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,(REAL-NS 1); :: thesis: for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) 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 (REAL-NS 1); :: thesis: for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) 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,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) 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,(REAL-NS n); :: thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) 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 (REAL-NS 1),(REAL-NS n); :: 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 ; :: thesis: ( not f is_differentiable_in x0 or ( 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-NS 1),REAL by Lm1;

assume 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)) ) )

then consider NN being Neighbourhood of x0 such that

A7: NN c= dom f and

A8: ex L being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) ex R being RestFunc of (REAL-NS 1),(REAL-NS n) st

for x being Point of (REAL-NS 1) st x in NN holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by NDIFF_1:def 6;

A9: I * J = id (REAL-NS 1) by Lm1, A1, Lm2, FUNCT_1:39;

A10: g * J = f * (id (REAL-NS 1)) by A9, A5, RELAT_1:36

.= f by FUNCT_2:17 ;

consider e being Real such that

A11: 0 < e and

A12: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } c= NN by NFCONT_1:def 1;

consider L being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))), R being RestFunc of (REAL-NS 1),(REAL-NS n) such that

A13: for x9 being Point of (REAL-NS 1) st x9 in NN holds

(f /. x9) - (f /. x0) = (L . (x9 - x0)) + (R /. (x9 - x0)) by A8;

reconsider R0 = R * I as RestFunc of (REAL-NS n) by A1, Th40;

L is LinearOperator of (REAL-NS 1),(REAL-NS n) by LOPBAN_1:def 9;

then reconsider L0 = L * I as LinearFunc of (REAL-NS n) by A1, Th40;

set N = { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ;

A14: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } c= the carrier of (REAL-NS 1)

set N0 = { z where z is Element of REAL : |.(z - y0).| < e } ;

A15: N c= dom f by A7, A12;

J .: (dom f) = J .: (J " (dom g)) by A10, RELAT_1:147;

then A24: J .: (dom f) = dom (f * I) by A5, Lm2, FUNCT_1:77;

A25: I * J = id (REAL 1) by A1, Lm2, FUNCT_1:39;

N c= dom f by A7, A12;

then A26: { z where z is Element of REAL : |.(z - y0).| < e } c= dom (f * I) by A24, A23, RELAT_1:123;

A27: ].(y0 - e),(y0 + e).[ c= { z where z is Element of REAL : |.(z - y0).| < e }

then A29: { z where z is Element of REAL : |.(z - y0).| < e } is Neighbourhood of y0 by A11, RCOMP_1:def 6;

N c= REAL 1 by A14, REAL_NS1:def 4;

then (I * J) .: N = N by A25, FRECHET:13;

then A30: I .: { z where z is Element of REAL : |.(z - y0).| < e } = N by A23, RELAT_1:126;

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

thus g is_differentiable_in y0 by A5, A31, A29, A26, NDIFF_3:def 3; :: thesis: ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

A44: diff ((f * I),y0) = L0 /. jj by A31, A43, A29, A26, NDIFF_3:def 4;

thus A45: diff (g,y0) = ((diff (f,x0)) * I) . 1 by A5, A44, A6, A13, A7, NDIFF_1:def 7

.= (diff (f,x0)) . (I . jj) by A1, FUNCT_1:13, PDIFF_1:2

.= (diff (f,x0)) . <*1*> by A1, Lm2 ; :: 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 (REAL-NS 1) by REAL_NS1:def 4;

A47: diff (f,x0) is LinearOperator of (REAL-NS 1),(REAL-NS n) 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 A46, REAL_NS1:3

.= r * (diff (g,y0)) by A45, A47, LOPBAN_1:def 5 ; :: thesis: verum

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) 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,(REAL-NS 1); :: thesis: for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) 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 (REAL-NS 1); :: thesis: for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) 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,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) 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,(REAL-NS n); :: thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) 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 (REAL-NS 1),(REAL-NS n); :: 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 ; :: thesis: ( not f is_differentiable_in x0 or ( 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-NS 1),REAL by Lm1;

assume 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)) ) )

then consider NN being Neighbourhood of x0 such that

A7: NN c= dom f and

A8: ex L being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) ex R being RestFunc of (REAL-NS 1),(REAL-NS n) st

for x being Point of (REAL-NS 1) st x in NN holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by NDIFF_1:def 6;

A9: I * J = id (REAL-NS 1) by Lm1, A1, Lm2, FUNCT_1:39;

A10: g * J = f * (id (REAL-NS 1)) by A9, A5, RELAT_1:36

.= f by FUNCT_2:17 ;

consider e being Real such that

A11: 0 < e and

A12: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } c= NN by NFCONT_1:def 1;

consider L being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))), R being RestFunc of (REAL-NS 1),(REAL-NS n) such that

A13: for x9 being Point of (REAL-NS 1) st x9 in NN holds

(f /. x9) - (f /. x0) = (L . (x9 - x0)) + (R /. (x9 - x0)) by A8;

reconsider R0 = R * I as RestFunc of (REAL-NS n) by A1, Th40;

L is LinearOperator of (REAL-NS 1),(REAL-NS n) by LOPBAN_1:def 9;

then reconsider L0 = L * I as LinearFunc of (REAL-NS n) by A1, Th40;

set N = { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ;

A14: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } c= the carrier of (REAL-NS 1)

proof

then reconsider N = { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } as Neighbourhood of x0 by A11, NFCONT_1:def 1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } or y in the carrier of (REAL-NS 1) )

assume y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ; :: thesis: y in the carrier of (REAL-NS 1)

then ex z being Point of (REAL-NS 1) st

( y = z & ||.(z - x0).|| < e ) ;

hence y in the carrier of (REAL-NS 1) ; :: thesis: verum

end;assume y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ; :: thesis: y in the carrier of (REAL-NS 1)

then ex z being Point of (REAL-NS 1) st

( y = z & ||.(z - x0).|| < e ) ;

hence y in the carrier of (REAL-NS 1) ; :: thesis: verum

set N0 = { z where z is Element of REAL : |.(z - y0).| < e } ;

A15: N c= dom f by A7, A12;

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 } ) )

then A23:
{ z where z is Element of REAL : |.(z - y0).| < e } = J .: N
by TARSKI:2;( ( 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 } ) )

then consider ww being object such that

ww in REAL 1 and

A19: ww in N and

A20: z = J . ww by FUNCT_2:64;

consider w being Point of (REAL-NS 1) such that

A21: ww = w and

A22: ||.(w - x0).|| < e by A19;

reconsider y9 = J . w as Element of REAL ;

J . x0 = y0 by A4, Lm2;

then J . (w - x0) = y9 - y0 by PDIFF_1:4;

then |.(y9 - y0).| < e by A22, PDIFF_1:4;

hence z in { z where z is Element of REAL : |.(z - y0).| < e } by A20, A21; :: thesis: verum

end;hereby :: thesis: ( z in J .: N implies z in { z where z is Element of REAL : |.(z - y0).| < e } )

assume
z in J .: N
; :: thesis: 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 (REAL-NS 1) ;

x0 = I . y0 by A1, A4, Lm2;

then w - x0 = I . (y9 - y0) by A1, Lm1, PDIFF_1:3;

then ||.(w - x0).|| = |.(y9 - y0).| by A1, Lm1, PDIFF_1:3;

then A18: w in { z0 where z0 is Point of (REAL-NS 1) : ||.(z0 - x0).|| < e } by A17;

J . (I . y9) = y9 by A1, Lm2, FUNCT_1:35;

hence z in J .: N by A18, A16, FUNCT_2:35; :: thesis: verum

end;then consider y9 being Element of REAL such that

A16: z = y9 and

A17: |.(y9 - y0).| < e ;

reconsider w = I . y9 as Point of (REAL-NS 1) ;

x0 = I . y0 by A1, A4, Lm2;

then w - x0 = I . (y9 - y0) by A1, Lm1, PDIFF_1:3;

then ||.(w - x0).|| = |.(y9 - y0).| by A1, Lm1, PDIFF_1:3;

then A18: w in { z0 where z0 is Point of (REAL-NS 1) : ||.(z0 - x0).|| < e } by A17;

J . (I . y9) = y9 by A1, Lm2, FUNCT_1:35;

hence z in J .: N by A18, A16, FUNCT_2:35; :: thesis: verum

then consider ww being object such that

ww in REAL 1 and

A19: ww in N and

A20: z = J . ww by FUNCT_2:64;

consider w being Point of (REAL-NS 1) such that

A21: ww = w and

A22: ||.(w - x0).|| < e by A19;

reconsider y9 = J . w as Element of REAL ;

J . x0 = y0 by A4, Lm2;

then J . (w - x0) = y9 - y0 by PDIFF_1:4;

then |.(y9 - y0).| < e by A22, PDIFF_1:4;

hence z in { z where z is Element of REAL : |.(z - y0).| < e } by A20, A21; :: thesis: verum

J .: (dom f) = J .: (J " (dom g)) by A10, RELAT_1:147;

then A24: J .: (dom f) = dom (f * I) by A5, Lm2, FUNCT_1:77;

A25: I * J = id (REAL 1) by A1, Lm2, FUNCT_1:39;

N c= dom f by A7, A12;

then A26: { z where z is Element of REAL : |.(z - y0).| < e } c= dom (f * I) by A24, A23, RELAT_1:123;

A27: ].(y0 - e),(y0 + e).[ c= { z where z is Element of REAL : |.(z - y0).| < e }

proof

end;

{ z where z is Element of REAL : |.(z - y0).| < e } c= ].(y0 - e),(y0 + e).[
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 }

hence
].(y0 - e),(y0 + e).[ c= { z where z is Element of REAL : |.(z - y0).| < e }
; :: thesis: verumd 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 }

reconsider y1 = d as Element of REAL by A28;

|.(y1 - y0).| < e by A28, RCOMP_1:1;

hence d in { z where z is Element of REAL : |.(z - y0).| < e } ; :: thesis: verum

end;assume A28: d in ].(y0 - e),(y0 + e).[ ; :: thesis: d in { z where z is Element of REAL : |.(z - y0).| < e }

reconsider y1 = d as Element of REAL by A28;

|.(y1 - y0).| < e by A28, RCOMP_1:1;

hence d in { z where z is Element of REAL : |.(z - y0).| < e } ; :: thesis: verum

proof

then
{ z where z is Element of REAL : |.(z - y0).| < e } = ].(y0 - e),(y0 + e).[
by A27, XBOOLE_0:def 10;
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;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

then A29: { z where z is Element of REAL : |.(z - y0).| < e } is Neighbourhood of y0 by A11, RCOMP_1:def 6;

N c= REAL 1 by A14, REAL_NS1:def 4;

then (I * J) .: N = N by A25, FRECHET:13;

then A30: I .: { z where z is Element of REAL : |.(z - y0).| < e } = N by A23, RELAT_1:126;

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

then A43:
f * I is_differentiable_in y0
by A29, A26, NDIFF_3:def 3;
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 (REAL-NS 1) ;

R is total by NDIFF_1:def 5;

then A32: dom R = the carrier of (REAL-NS 1) 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 A33, FUNCT_1:12;

then A34: R /. (I . (y1 - y0)) = R0 /. dy1y0 by A33, PARTFUN1:def 6;

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 A30, FUNCT_2:35;

then A38: f /. (I . y1) = f . (I . y1) by A15, PARTFUN1:def 6;

f /. (I . y1) = (f * I) . y1 by A38, A26, A36, FUNCT_1:12;

then A39: f /. (I . y1) = (f * I) /. y1 by A26, A36, PARTFUN1:def 6;

A40: x0 = I . y0 by A4, A1, Lm2;

then f /. (I . y0) = f . (I . y0) by A2, PARTFUN1:def 6;

then f /. (I . y0) = (f * I) . y0 by A3, A5, FUNCT_1:12;

then A41: f /. (I . y0) = (f * I) /. y0 by A3, A5, PARTFUN1:def 6;

reconsider d = y1 - y0 as Element of REAL by XREAL_0:def 1;

(f /. y9) - (f /. x0) = (L . (y9 - x0)) + (R /. (y9 - x0)) by A13, A12, A37;

then A42: (f /. (I . y1)) - (f /. (I . y0)) = (L . (I . d)) + (R /. (y9 - x0)) by A1, A40, Lm1, PDIFF_1:3;

L . (I . d) = L0 /. dy1y0 by A35, FUNCT_1:12;

hence ((f * I) /. y1) - ((f * I) /. y0) = (L0 /. (y1 - y0)) + (R0 /. (y1 - y0)) by A40, A42, A34, A39, A41, A1, Lm1, PDIFF_1:3; :: thesis: verum

end;reconsider yy = y1 as Element of REAL by XREAL_0:def 1;

reconsider y9 = I . yy as Point of (REAL-NS 1) ;

R is total by NDIFF_1:def 5;

then A32: dom R = the carrier of (REAL-NS 1) 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 A33, FUNCT_1:12;

then A34: R /. (I . (y1 - y0)) = R0 /. dy1y0 by A33, PARTFUN1:def 6;

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 A30, FUNCT_2:35;

then A38: f /. (I . y1) = f . (I . y1) by A15, PARTFUN1:def 6;

f /. (I . y1) = (f * I) . y1 by A38, A26, A36, FUNCT_1:12;

then A39: f /. (I . y1) = (f * I) /. y1 by A26, A36, PARTFUN1:def 6;

A40: x0 = I . y0 by A4, A1, Lm2;

then f /. (I . y0) = f . (I . y0) by A2, PARTFUN1:def 6;

then f /. (I . y0) = (f * I) . y0 by A3, A5, FUNCT_1:12;

then A41: f /. (I . y0) = (f * I) /. y0 by A3, A5, PARTFUN1:def 6;

reconsider d = y1 - y0 as Element of REAL by XREAL_0:def 1;

(f /. y9) - (f /. x0) = (L . (y9 - x0)) + (R /. (y9 - x0)) by A13, A12, A37;

then A42: (f /. (I . y1)) - (f /. (I . y0)) = (L . (I . d)) + (R /. (y9 - x0)) by A1, A40, Lm1, PDIFF_1:3;

L . (I . d) = L0 /. dy1y0 by A35, FUNCT_1:12;

hence ((f * I) /. y1) - ((f * I) /. y0) = (L0 /. (y1 - y0)) + (R0 /. (y1 - y0)) by A40, A42, A34, A39, A41, A1, Lm1, PDIFF_1:3; :: thesis: verum

thus g is_differentiable_in y0 by A5, A31, A29, A26, NDIFF_3:def 3; :: thesis: ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

A44: diff ((f * I),y0) = L0 /. jj by A31, A43, A29, A26, NDIFF_3:def 4;

thus A45: diff (g,y0) = ((diff (f,x0)) * I) . 1 by A5, A44, A6, A13, A7, NDIFF_1:def 7

.= (diff (f,x0)) . (I . jj) by A1, FUNCT_1:13, PDIFF_1:2

.= (diff (f,x0)) . <*1*> by A1, Lm2 ; :: 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 (REAL-NS 1) by REAL_NS1:def 4;

A47: diff (f,x0) is LinearOperator of (REAL-NS 1),(REAL-NS n) 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 A46, REAL_NS1:3

.= r * (diff (g,y0)) by A45, A47, LOPBAN_1:def 5 ; :: thesis: verum