let X be set ; :: thesis: for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n) holds

( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X )

let n be non zero Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n) holds

( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X )

let f be PartFunc of REAL,(REAL n); :: thesis: ( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X )

thus ( f is_differentiable_on X implies for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X ) by Th29; :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X ) implies f is_differentiable_on X )

assume A1: for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X ; :: thesis: f is_differentiable_on X

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * g is_differentiable_on X by A1;

then A2: g is_differentiable_on X by Th30;

then A3: X is open Subset of REAL by NDIFF_3:9, NDIFF_3:11;

then A4: X c= dom f by A2, NDIFF_3:10;

for x being Real st x in X holds

f is_differentiable_in x by A3, A2, NDIFF_3:10;

hence f is_differentiable_on X by A3, A4, Th5; :: thesis: verum

for f being PartFunc of REAL,(REAL n) holds

( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X )

let n be non zero Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n) holds

( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X )

let f be PartFunc of REAL,(REAL n); :: thesis: ( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X )

thus ( f is_differentiable_on X implies for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X ) by Th29; :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X ) implies f is_differentiable_on X )

assume A1: for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X ; :: thesis: f is_differentiable_on X

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * g is_differentiable_on X by A1;

then A2: g is_differentiable_on X by Th30;

then A3: X is open Subset of REAL by NDIFF_3:9, NDIFF_3:11;

then A4: X c= dom f by A2, NDIFF_3:10;

for x being Real st x in X holds

f is_differentiable_in x by A3, A2, NDIFF_3:10;

hence f is_differentiable_on X by A3, A4, Th5; :: thesis: verum