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:
A1: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
A2: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
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;

hereby :: thesis:

assume A3: f is_differentiable_in x ; :: thesis:
thus 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 ) :: thesis:

proof

let i be Nat; :: thesis:
assume A4: ( 1 <= i & i <= n ) ; :: thesis:
reconsider fi = (Proj (i,n)) * f0 as PartFunc of (REAL m),(REAL 1) by A2, REAL_NS1:def 4;
take fi ; :: thesis:
thus fi = (Proj (i,n)) * f ; :: thesis:
thus fi is_differentiable_in x by A3, A4, PDIFF_6:29; :: thesis:

end;

end;

assume A5: 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 ) ; :: thesis:
for i being Nat st 1 <= i & i <= n holds
(Proj (i,n)) * f0 is_differentiable_in x0

proof

let i be Nat; :: thesis:
assume ( 1 <= i & i <= n ) ; :: thesis:
then consider fi being PartFunc of (REAL m),(REAL 1) such that
A6: ( fi = (Proj (i,n)) * f & fi is_differentiable_in x ) by A5;
thus (Proj (i,n)) * f0 is_differentiable_in x0 by A6; :: thesis:

end;

hence f is_differentiable_in x by PDIFF_6:29; :: thesis: