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

for x0 being Real holds

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

(Proj (i,n)) * f is_differentiable_in x0 )

let f be PartFunc of REAL,(REAL n); :: thesis: for x0 being Real holds

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

(Proj (i,n)) * f is_differentiable_in x0 )

let x0 be Real; :: thesis: ( f is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_in x0 )

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

(Proj (i,n)) * f is_differentiable_in x0 ) by Th25; :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_in x0 ) implies f is_differentiable_in x0 )

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

(Proj (i,n)) * f is_differentiable_in x0 ; :: thesis: f is_differentiable_in x0

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_in x0 by A1;

then g is_differentiable_in x0 by Th25;

hence f is_differentiable_in x0 ; :: thesis: verum

for x0 being Real holds

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

(Proj (i,n)) * f is_differentiable_in x0 )

let f be PartFunc of REAL,(REAL n); :: thesis: for x0 being Real holds

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

(Proj (i,n)) * f is_differentiable_in x0 )

let x0 be Real; :: thesis: ( f is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_in x0 )

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

(Proj (i,n)) * f is_differentiable_in x0 ) by Th25; :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_in x0 ) implies f is_differentiable_in x0 )

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

(Proj (i,n)) * f is_differentiable_in x0 ; :: thesis: f is_differentiable_in x0

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_in x0 by A1;

then g is_differentiable_in x0 by Th25;

hence f is_differentiable_in x0 ; :: thesis: verum