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;

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

hence
g is_differentiable_on X
by A3, A6, NDIFF_3:10; :: thesis: verumg 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

end;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

hence
g is_differentiable_in x
by Th25; :: thesis: verum(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;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