let X be set ; 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 ; 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); ( 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; ( ( 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
; 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; verum