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