let m, n be non zero Nat; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
for i being Nat
for fi being PartFunc of (REAL m),REAL st 1 <= i & i <= n & fi = (proj (i,n)) * f holds
( fi is_differentiable_in x & diff (fi,x) = (proj (i,n)) * (diff (f,x)) )
let f be PartFunc of (REAL m),(REAL n); :: thesis: for x being Element of REAL m st f is_differentiable_in x holds
for i being Nat
for fi being PartFunc of (REAL m),REAL st 1 <= i & i <= n & fi = (proj (i,n)) * f holds
( fi is_differentiable_in x & diff (fi,x) = (proj (i,n)) * (diff (f,x)) )
let x be Element of REAL m; :: thesis: ( f is_differentiable_in x implies for i being Nat
for fi being PartFunc of (REAL m),REAL st 1 <= i & i <= n & fi = (proj (i,n)) * f holds
( fi is_differentiable_in x & diff (fi,x) = (proj (i,n)) * (diff (f,x)) ) )
A1: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
assume A2: f is_differentiable_in x ; :: thesis: for i being Nat
for fi being PartFunc of (REAL m),REAL st 1 <= i & i <= n & fi = (proj (i,n)) * f holds
( fi is_differentiable_in x & diff (fi,x) = (proj (i,n)) * (diff (f,x)) )
let i be Nat; :: thesis: for fi being PartFunc of (REAL m),REAL st 1 <= i & i <= n & fi = (proj (i,n)) * f holds
( fi is_differentiable_in x & diff (fi,x) = (proj (i,n)) * (diff (f,x)) )
let fi be PartFunc of (REAL m),REAL; :: thesis: ( 1 <= i & i <= n & fi = (proj (i,n)) * f implies ( fi is_differentiable_in x & diff (fi,x) = (proj (i,n)) * (diff (f,x)) ) )
assume A3: ( 1 <= i & i <= n & fi = (proj (i,n)) * f ) ; :: thesis: ( fi is_differentiable_in x & diff (fi,x) = (proj (i,n)) * (diff (f,x)) )
then A4: ex fi being PartFunc of (REAL m),REAL st
( fi = (proj (i,n)) * f & fi is_differentiable_in x ) by A2, Th19;
hence fi is_differentiable_in x by A3; :: thesis: diff (fi,x) = (proj (i,n)) * (diff (f,x))
reconsider f0 = f as PartFunc of (REAL-NS m),(REAL-NS n) by A1;
reconsider x0 = x as Point of (REAL-NS m) by REAL_NS1:def 4;
A5: (Proj (i,n)) * (diff (f0,x0)) = diff (((Proj (i,n)) * f0),x0) by A2, A3, PDIFF_6:28;
A6: (Proj (i,n)) * f0 = (((proj (1,1)) ") * (proj (i,n))) * f0 by PDIFF_1:11
.= <>* fi by A3, RELAT_1:36 ;
A7: (Proj (i,n)) * (diff (f0,x0)) = diff ((<>* fi),x) by A3, A4, A5, A6, PDIFF_6:3, PDIFF_7:def 1;
A8: diff (fi,x) = (proj (1,1)) * (diff ((<>* fi),x)) by PDIFF_7:def 2
.= (proj (1,1)) * ((Proj (i,n)) * (diff (f,x))) by A2, A7, PDIFF_6:3
.= ((proj (1,1)) * (Proj (i,n))) * (diff (f,x)) by RELAT_1:36 ;
1 in Seg 1 ;
then A9: rng (proj (1,1)) = REAL by PDIFF_1:1;
(proj (1,1)) * (Proj (i,n)) = (proj (1,1)) * (((proj (1,1)) ") * (proj (i,n))) by PDIFF_1:11
.= ((proj (1,1)) * ((proj (1,1)) ")) * (proj (i,n)) by RELAT_1:36
.= (id REAL) * (proj (i,n)) by A9, FUNCT_1:39
.= proj (i,n) by FUNCT_2:17 ;
hence diff (fi,x) = (proj (i,n)) * (diff (f,x)) by A8; :: thesis: verum