let m, n be non zero Nat; :: thesis:
let f be PartFunc of (REAL m),(REAL n); :: thesis:
let x be Element of REAL m; :: thesis:
assume A1: f is_differentiable_in x ; :: thesis:
set M = Jacobian (f,x);
A2: ( the carrier of (TOP-REAL n) = REAL n & the carrier of (TOP-REAL m) = REAL m ) by EUCLID:22;
for dx being Element of REAL m holds (diff (f,x)) . dx = (Mx2Tran (Jacobian (f,x))) . dx

let dx be Element of REAL m; :: thesis:
reconsider fdx = (diff (f,x)) . dx as Element of REAL n ;
reconsider Mdx = (Mx2Tran (Jacobian (f,x))) . dx as Element of REAL n by A2, FUNCT_2:5;
A3: len fdx = n by CARD_1:def 7;
A4: len Mdx = n by CARD_1:def 7;
for j being Nat st 1 <= j & j <= len fdx holds
fdx . j = Mdx . j

let j be Nat; :: thesis:
assume A5: ( 1 <= j & j <= len fdx ) ; :: thesis:
then consider fj being PartFunc of (REAL m),REAL such that
A6: ( fj = (proj (j,n)) * f & fj is_differentiable_in x ) by A1, A3, Th19;
consider dy being FinSequence of REAL such that
A7: ( dom dy = Seg m & ( for i being Nat st 1 <= i & i <= m holds
dy . i = ((proj (i,m)) . dx) * (partdiff (fj,x,i)) ) & (diff (fj,x)) . dx = Sum dy ) by A6, Th26;
A8: j in Seg n by A3, A5;
A9: for i being Nat st i in Seg m holds
(Jacobian (f,x)) * (i,j) = partdiff (fj,x,i)

let i be Nat; :: thesis:
assume i in Seg m ; :: thesis:
hence (Jacobian (f,x)) * (i,j) = partdiff (f,x,i,j) by A8, Def1
.= partdiff (fj,x,i) by A6 ;
:: thesis:

end;

A10: for i being Nat st 1 <= i & i <= m holds
dy . i = ((proj (i,m)) . dx) * ((Jacobian (f,x)) * (i,j))

let i be Nat; :: thesis:
assume A11: ( 1 <= i & i <= m ) ; :: thesis:
then A12: i in Seg m ;
thus dy . i = ((proj (i,m)) . dx) * (partdiff (fj,x,i)) by A7, A11
.= ((proj (i,m)) . dx) * ((Jacobian (f,x)) * (i,j)) by A9, A12 ; :: thesis:

end;

set dxM = (LineVec2Mx (@ dx)) * (Jacobian (f,x));
A13: ( len (Jacobian (f,x)) = m & width (Jacobian (f,x)) = n & Indices (Jacobian (f,x)) = [:(Seg m),(Seg n):] ) by MATRIX_0:23;
A14: ( LineVec2Mx (@ dx) = <*(@ dx)*> & LineVec2Mx (@ dx) is Matrix of 1, len (@ dx),F_Real ) by MATRIX15:def 1;
A15: len (@ dx) = len dx by MATRTOP1:def 1
.= m by CARD_1:def 7 ;
then A16: ( len (LineVec2Mx (@ dx)) = 1 & width (LineVec2Mx (@ dx)) = m & Indices (LineVec2Mx (@ dx)) = [:(Seg 1),(Seg m):] ) by MATRIX_0:23;
then A17: ( len ((LineVec2Mx (@ dx)) * (Jacobian (f,x))) = len (LineVec2Mx (@ dx)) & width ((LineVec2Mx (@ dx)) * (Jacobian (f,x))) = width (Jacobian (f,x)) & ( for i, j being Nat st [i,j] in Indices ((LineVec2Mx (@ dx)) * (Jacobian (f,x))) holds
((LineVec2Mx (@ dx)) * (Jacobian (f,x))) * (i,j) = (Line ((LineVec2Mx (@ dx)),i)) "*" (Col ((Jacobian (f,x)),j)) ) ) by A13, MATRIX_3:def 4;
A18: Mdx = Line (((LineVec2Mx (@ dx)) * (Jacobian (f,x))),1) by MATRTOP1:def 3;
A19: j in Seg (width ((LineVec2Mx (@ dx)) * (Jacobian (f,x)))) by A3, A5, A13, A17;
then A20: Mdx . j = ((LineVec2Mx (@ dx)) * (Jacobian (f,x))) * (1,j) by A18, MATRIX_0:def 7;
len ((LineVec2Mx (@ dx)) * (Jacobian (f,x))) = 1 by A16, MATRIX_3:def 4, A13;
then dom ((LineVec2Mx (@ dx)) * (Jacobian (f,x))) = Seg 1 by FINSEQ_1:def 3;
then 1 in dom ((LineVec2Mx (@ dx)) * (Jacobian (f,x))) ;
then [1,j] in Indices ((LineVec2Mx (@ dx)) * (Jacobian (f,x))) by A19, ZFMISC_1:87;
then A22: Mdx . j = (Line ((LineVec2Mx (@ dx)),1)) "*" (Col ((Jacobian (f,x)),j)) by A13, A16, A20, MATRIX_3:def 4;
set u = mlt ((Line ((LineVec2Mx (@ dx)),1)),(Col ((Jacobian (f,x)),j)));
len (Line ((LineVec2Mx (@ dx)),1)) = width (LineVec2Mx (@ dx)) by MATRIX_0:def 7
.= m by A15, MATRIX_0:23 ;
then reconsider a = Line ((LineVec2Mx (@ dx)),1) as Element of m -tuples_on the carrier of F_Real by FINSEQ_2:92;
len (Col ((Jacobian (f,x)),j)) = len (Jacobian (f,x)) by MATRIX_0:def 8
.= m by MATRIX_0:23 ;
then reconsider b = Col ((Jacobian (f,x)),j) as Element of m -tuples_on the carrier of F_Real by FINSEQ_2:92;
mlt ((Line ((LineVec2Mx (@ dx)),1)),(Col ((Jacobian (f,x)),j))) = mlt (a,b) ;
then mlt ((Line ((LineVec2Mx (@ dx)),1)),(Col ((Jacobian (f,x)),j))) in { s where s is Element of the carrier of F_Real * : len s = m } ;
then A23: ex u0 being Element of the carrier of F_Real * st
( u0 = mlt ((Line ((LineVec2Mx (@ dx)),1)),(Col ((Jacobian (f,x)),j))) & len u0 = m ) ;
m is Element of NAT by ORDINAL1:def 12;
then A24: len dy = m by A7, FINSEQ_1:def 3;
A25: for i being Nat st 1 <= i & i <= len dy holds
dy . i = (mlt ((Line ((LineVec2Mx (@ dx)),1)),(Col ((Jacobian (f,x)),j)))) . i

let i be Nat; :: thesis:
assume A26: ( 1 <= i & i <= len dy ) ; :: thesis:
then A27: i in Seg m by A24;
reconsider s = (proj (i,m)) . dx as Element of F_Real ;
reconsider t = (Jacobian (f,x)) * (i,j) as Element of F_Real ;
1 in Seg 1 ;
then [1,i] in Indices (LineVec2Mx (@ dx)) by A16, A27, ZFMISC_1:87;
then A28: ex p being FinSequence of the carrier of F_Real st
( p = (LineVec2Mx (@ dx)) . 1 & (LineVec2Mx (@ dx)) * (1,i) = p . i ) by MATRIX_0:def 5;
(LineVec2Mx (@ dx)) . 1 = @ dx by A14
.= dx by MATRTOP1:def 1 ;
then a . i = dx . i by A16, A27, A28, MATRIX_0:def 7;
then A30: a . i = (proj (i,m)) . dx by PDIFF_1:def 1;
i in dom (Jacobian (f,x)) by A13, A27, FINSEQ_1:def 3;
then b . i = (Jacobian (f,x)) * (i,j) by MATRIX_0:def 8;
then (mlt ((Line ((LineVec2Mx (@ dx)),1)),(Col ((Jacobian (f,x)),j)))) . i = s * t by A27, A30, FVSUM_1:61
.= ((proj (i,m)) . dx) * ((Jacobian (f,x)) * (i,j)) ;
hence dy . i = (mlt ((Line ((LineVec2Mx (@ dx)),1)),(Col ((Jacobian (f,x)),j)))) . i by A10, A24, A26; :: thesis:

end;

A33: dom (diff (f,x)) = REAL m by FUNCT_2:def 1;
(diff (fj,x)) . dx = ((proj (j,n)) * (diff (f,x))) . dx by A1, A3, A5, A6, Th20
.= (proj (j,n)) . ((diff (f,x)) . dx) by A33, FUNCT_1:13
.= fdx . j by PDIFF_1:def 1 ;
hence fdx . j = Mdx . j by A7, A22, A23, A24, A25, FINSEQ_1:14; :: thesis:

end;

hence (diff (f,x)) . dx = (Mx2Tran (Jacobian (f,x))) . dx by A4, FINSEQ_1:14, CARD_1:def 7; :: thesis:

end;

hence diff (f,x) = Mx2Tran (Jacobian (f,x)) by EUCLID:22; :: thesis: