let m be non zero Nat; :: thesis: for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x holds
for dx being Element of REAL m ex dy being FinSequence of REAL st
( dom dy = Seg m & ( for i being Nat st 1 <= i & i <= m holds
dy . i = ((proj (i,m)) . dx) * (partdiff (f,x,i)) ) & (diff (f,x)) . dx = Sum dy )
let f be PartFunc of (REAL m),REAL; :: thesis: for x being Element of REAL m st f is_differentiable_in x holds
for dx being Element of REAL m ex dy being FinSequence of REAL st
( dom dy = Seg m & ( for i being Nat st 1 <= i & i <= m holds
dy . i = ((proj (i,m)) . dx) * (partdiff (f,x,i)) ) & (diff (f,x)) . dx = Sum dy )
let x be Element of REAL m; :: thesis: ( f is_differentiable_in x implies for dx being Element of REAL m ex dy being FinSequence of REAL st
( dom dy = Seg m & ( for i being Nat st 1 <= i & i <= m holds
dy . i = ((proj (i,m)) . dx) * (partdiff (f,x,i)) ) & (diff (f,x)) . dx = Sum dy ) )
assume A1: f is_differentiable_in x ; :: thesis: for dx being Element of REAL m ex dy being FinSequence of REAL st
( dom dy = Seg m & ( for i being Nat st 1 <= i & i <= m holds
dy . i = ((proj (i,m)) . dx) * (partdiff (f,x,i)) ) & (diff (f,x)) . dx = Sum dy )
let dx be Element of REAL m; :: thesis: ex dy being FinSequence of REAL st
( dom dy = Seg m & ( for i being Nat st 1 <= i & i <= m holds
dy . i = ((proj (i,m)) . dx) * (partdiff (f,x,i)) ) & (diff (f,x)) . dx = Sum dy )
consider s being FinSequence of REAL m such that
A2: ( dom s = Seg m & ( for i being Nat st 1 <= i & i <= m holds
ex ei being Element of REAL m st
( ei = (reproj (i,(0* m))) . 1 & s . i = ((proj (i,m)) . dx) * ei ) ) & Sum s = dx ) by Th5;
deffunc H₁( Nat) -> Element of REAL = In (((diff (f,x)) . (s . $1)),REAL);
consider dy being FinSequence of REAL such that
A3: ( len dy = m & ( for i being Nat st i in dom dy holds
dy . i = H₁(i) ) ) from FINSEQ_2:sch 1();
A4: dom dy = Seg m by A3, FINSEQ_1:def 3;
A5: for i being Nat st i in dom dy holds
dy . i = (diff (f,x)) . (s . i)

proof

let i be Nat; :: thesis: ( i in dom dy implies dy . i = (diff (f,x)) . (s . i) )
assume i in dom dy ; :: thesis: dy . i = (diff (f,x)) . (s . i)
then dy . i = In (((diff (f,x)) . (s . i)),REAL) by A3;
hence dy . i = (diff (f,x)) . (s . i) ; :: thesis: verum

end;

take dy ; :: thesis: ( dom dy = Seg m & ( for i being Nat st 1 <= i & i <= m holds
dy . i = ((proj (i,m)) . dx) * (partdiff (f,x,i)) ) & (diff (f,x)) . dx = Sum dy )
thus dom dy = Seg m by A3, FINSEQ_1:def 3; :: thesis: ( ( for i being Nat st 1 <= i & i <= m holds
dy . i = ((proj (i,m)) . dx) * (partdiff (f,x,i)) ) & (diff (f,x)) . dx = Sum dy )
thus for i being Nat st 1 <= i & i <= m holds
dy . i = ((proj (i,m)) . dx) * (partdiff (f,x,i)) :: thesis: (diff (f,x)) . dx = Sum dy

proof

let i be Nat; :: thesis: ( 1 <= i & i <= m implies dy . i = ((proj (i,m)) . dx) * (partdiff (f,x,i)) )
assume A6: ( 1 <= i & i <= m ) ; :: thesis: dy . i = ((proj (i,m)) . dx) * (partdiff (f,x,i))
then A7: i in dom dy by A4;
consider ei being Element of REAL m such that
A8: ( ei = (reproj (i,(0* m))) . 1 & s . i = ((proj (i,m)) . dx) * ei ) by A2, A6;
thus dy . i = (diff (f,x)) . (s . i) by A5, A7
.= ((proj (i,m)) . dx) * ((diff (f,x)) . ei) by A1, A8, Th24
.= ((proj (i,m)) . dx) * (partdiff (f,x,i)) by A1, A6, A8, PDIFF_7:23 ; :: thesis: verum

end;

thus (diff (f,x)) . dx = Sum dy by A1, A2, A4, A5, Th25; :: thesis: verum