let X be set ; :: thesis:
let n be non zero Element of NAT ; :: thesis:
let g be PartFunc of REAL,(REAL-NS n); :: thesis:
thus ( g is_differentiable_on X implies for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_on X ) by Th28; :: thesis:
assume A1: for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_on X ; :: thesis:
1 <= n by NAT_1:14;
then A2: (Proj (1,n)) * g is_differentiable_on X by A1;
then A3: X is open Subset of REAL by NDIFF_3:9, NDIFF_3:11;
A4: dom (Proj (1,n)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;
A5: rng g c= the carrier of (REAL-NS n) ;
X c= dom ((Proj (1,n)) * g) by A2, A3, NDIFF_3:10;
then A6: X c= dom g by A5, A4, RELAT_1:27;

let x be Real; :: thesis:
assume A7: x in X ; :: thesis:

let i be Element of NAT ; :: thesis:
assume ( 1 <= i & i <= n ) ; :: thesis:
then (Proj (i,n)) * g is_differentiable_on X by A1;
hence (Proj (i,n)) * g is_differentiable_in x by A7, A3, NDIFF_3:10; :: thesis:

end;

hence g is_differentiable_in x by Th25; :: thesis:

end;

hence g is_differentiable_on X by A3, A6, NDIFF_3:10; :: thesis: