let n be non zero Element of NAT ; :: thesis: for a, b being Real
for f being PartFunc of REAL,(REAL-NS n) st ].a,b.[ c= dom f & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (f,x) = 0. (REAL-NS n) ) holds
f | ].a,b.[ is constant
let a, b be Real; :: thesis: for f being PartFunc of REAL,(REAL-NS n) st ].a,b.[ c= dom f & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (f,x) = 0. (REAL-NS n) ) holds
f | ].a,b.[ is constant
let f be PartFunc of REAL,(REAL-NS n); :: thesis: ( ].a,b.[ c= dom f & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (f,x) = 0. (REAL-NS n) ) implies f | ].a,b.[ is constant )
assume A1: ( ].a,b.[ c= dom f & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (f,x) = 0. (REAL-NS n) ) ) ; :: thesis: f | ].a,b.[ is constant
reconsider Z = ].a,b.[ as open Subset of REAL ;

now :: thesis: for i being Nat st 1 <= i & i <= n holds
((proj (i,n)) * f) | ].a,b.[ is constant

let i be Nat; :: thesis: ( 1 <= i & i <= n implies ((proj (i,n)) * f) | ].a,b.[ is constant )
assume A2: ( 1 <= i & i <= n ) ; :: thesis: ((proj (i,n)) * f) | ].a,b.[ is constant

A3: now :: thesis: for x being Real st x in Z holds
( (proj (i,n)) * f is_differentiable_in x & (proj (i,n)) . (diff (f,x)) = diff (((proj (i,n)) * f),x) )

let x be Real; :: thesis: ( x in Z implies ( (proj (i,n)) * f is_differentiable_in x & (proj (i,n)) . (diff (f,x)) = diff (((proj (i,n)) * f),x) ) )
assume x in Z ; :: thesis: ( (proj (i,n)) * f is_differentiable_in x & (proj (i,n)) . (diff (f,x)) = diff (((proj (i,n)) * f),x) )
then f is_differentiable_in x by A1, NDIFF_3:10;
hence ( (proj (i,n)) * f is_differentiable_in x & (proj (i,n)) . (diff (f,x)) = diff (((proj (i,n)) * f),x) ) by A2, Th39; :: thesis: verum

end;

A4: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;
dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng f c= dom (proj (i,n)) by A4;
then A5: Z c= dom ((proj (i,n)) * f) by A1, RELAT_1:27;
for x being Real st x in Z holds
(proj (i,n)) * f is_differentiable_in x by A3;
then A6: (proj (i,n)) * f is_differentiable_on ].a,b.[ by A5, FDIFF_1:9;
for x being Real st x in ].a,b.[ holds
diff (((proj (i,n)) * f),x) = 0

proof

let x be Real; :: thesis: ( x in ].a,b.[ implies diff (((proj (i,n)) * f),x) = 0 )
assume A7: x in ].a,b.[ ; :: thesis: diff (((proj (i,n)) * f),x) = 0
then A8: (proj (i,n)) . (diff (f,x)) = diff (((proj (i,n)) * f),x) by A3;
diff (f,x) = 0. (REAL-NS n) by A1, A7;
hence diff (((proj (i,n)) * f),x) = 0 by Lm7, A8; :: thesis: verum

end;

hence ((proj (i,n)) * f) | ].a,b.[ is constant by A6, ROLLE:7; :: thesis: verum

end;

hence f | ].a,b.[ is constant by Th40; :: thesis: verum