let m, n be non zero Nat; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m holds
( f is_differentiable_in x iff for i being Nat st 1 <= i & i <= n holds
ex fi being PartFunc of (REAL m),REAL st
( fi = (proj (i,n)) * f & fi is_differentiable_in x ) )
let f be PartFunc of (REAL m),(REAL n); :: thesis: for x being Element of REAL m holds
( f is_differentiable_in x iff for i being Nat st 1 <= i & i <= n holds
ex fi being PartFunc of (REAL m),REAL st
( fi = (proj (i,n)) * f & fi is_differentiable_in x ) )
let x be Element of REAL m; :: thesis: ( f is_differentiable_in x iff for i being Nat st 1 <= i & i <= n holds
ex fi being PartFunc of (REAL m),REAL st
( fi = (proj (i,n)) * f & fi is_differentiable_in x ) )
reconsider y = x as Point of (REAL-NS m) by REAL_NS1:def 4;
A2: for i being Nat holds <>* ((proj (i,n)) * f) = (Proj (i,n)) * f

proof

let i be Nat; :: thesis: <>* ((proj (i,n)) * f) = (Proj (i,n)) * f
reconsider fi = (proj (i,n)) * f as PartFunc of (REAL m),REAL ;
(Proj (i,n)) * f = (((proj (1,1)) ") * (proj (i,n))) * f by PDIFF_1:11
.= <>* fi by RELAT_1:36 ;
hence <>* ((proj (i,n)) * f) = (Proj (i,n)) * f ; :: thesis: verum

end;

hereby :: thesis: ( ( for i being Nat st 1 <= i & i <= n holds
ex fi being PartFunc of (REAL m),REAL st
( fi = (proj (i,n)) * f & fi is_differentiable_in x ) ) implies f is_differentiable_in x )

assume A3: f is_differentiable_in x ; :: thesis: for i being Nat st 1 <= i & i <= n holds
ex fi being PartFunc of (REAL m),REAL st
( fi = (proj (i,n)) * f & fi is_differentiable_in x )
thus for i being Nat st 1 <= i & i <= n holds
ex fi being PartFunc of (REAL m),REAL st
( fi = (proj (i,n)) * f & fi is_differentiable_in x ) :: thesis: verum

proof

let i be Nat; :: thesis: ( 1 <= i & i <= n implies ex fi being PartFunc of (REAL m),REAL st
( fi = (proj (i,n)) * f & fi is_differentiable_in x ) )
assume ( 1 <= i & i <= n ) ; :: thesis: ex fi being PartFunc of (REAL m),REAL st
( fi = (proj (i,n)) * f & fi is_differentiable_in x )
then consider Fi being PartFunc of (REAL m),(REAL 1) such that
A4: ( Fi = (Proj (i,n)) * f & Fi is_differentiable_in x ) by A3, Th18;
reconsider fi = (proj (i,n)) * f as PartFunc of (REAL m),REAL ;
take fi ; :: thesis: ( fi = (proj (i,n)) * f & fi is_differentiable_in x )
thus fi = (proj (i,n)) * f ; :: thesis: fi is_differentiable_in x
<>* fi = Fi by A4, A2;
hence fi is_differentiable_in x by A4, PDIFF_7:def 1; :: thesis: verum

end;

end;

assume A5: for i being Nat st 1 <= i & i <= n holds
ex fi being PartFunc of (REAL m),REAL st
( fi = (proj (i,n)) * f & fi is_differentiable_in x ) ; :: thesis: f is_differentiable_in x
for i being Nat st 1 <= i & i <= n holds
ex Fi being PartFunc of (REAL m),(REAL 1) st
( Fi = (Proj (i,n)) * f & Fi is_differentiable_in x )

proof

let i be Nat; :: thesis: ( 1 <= i & i <= n implies ex Fi being PartFunc of (REAL m),(REAL 1) st
( Fi = (Proj (i,n)) * f & Fi is_differentiable_in x ) )
assume ( 1 <= i & i <= n ) ; :: thesis: ex Fi being PartFunc of (REAL m),(REAL 1) st
( Fi = (Proj (i,n)) * f & Fi is_differentiable_in x )
then consider fi being PartFunc of (REAL m),REAL such that
A6: ( fi = (proj (i,n)) * f & fi is_differentiable_in x ) by A5;
reconsider Fi = (Proj (i,n)) * f as PartFunc of (REAL m),(REAL 1) by REAL_NS1:def 4;
take Fi ; :: thesis: ( Fi = (Proj (i,n)) * f & Fi is_differentiable_in x )
thus Fi = (Proj (i,n)) * f ; :: thesis: Fi is_differentiable_in x
Fi = <>* fi by A2, A6;
hence Fi is_differentiable_in x by A6, PDIFF_7:def 1; :: thesis: verum

end;

hence f is_differentiable_in x by Th18; :: thesis: verum