let X be set ; :: thesis: for n being non zero Element of NAT
for g being PartFunc of REAL,(REAL-NS n) holds
( g is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_on X )
let n be non zero Element of NAT ; :: thesis: for g being PartFunc of REAL,(REAL-NS n) holds
( g is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_on X )
let g be PartFunc of REAL,(REAL-NS n); :: thesis: ( g is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_on X )
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: ( ( for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_on X ) implies g is_differentiable_on X )
assume A1: for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_on X ; :: thesis: g is_differentiable_on X
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;

now :: thesis: for x being Real st x in X holds
g is_differentiable_in x

let x be Real; :: thesis: ( x in X implies g is_differentiable_in x )
assume A7: x in X ; :: thesis: g is_differentiable_in x

now :: thesis: for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies (Proj (i,n)) * g is_differentiable_in x )
assume ( 1 <= i & i <= n ) ; :: thesis: (Proj (i,n)) * g is_differentiable_in x
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: verum

end;

hence g is_differentiable_in x by Th25; :: thesis: verum

end;

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