let p be Element of REAL 3; :: thesis: for f being PartFunc of (REAL 3),REAL st f is total & f is constant holds
grad f,p = 0.REAL 3
let f be PartFunc of (REAL 3),REAL ; :: thesis: ( f is total & f is constant implies grad f,p = 0.REAL 3 )
assume A0: ( f is total & f is constant ) ; :: thesis: grad f,p = 0.REAL 3
A2: dom f = REAL 3 by A0, FUNCT_2:def 1;
REAL = [#] REAL ;
then reconsider W = REAL as open Subset of REAL ;
consider a being Real such that
A3: for p being Element of REAL 3 st p in REAL 3 holds
f . p = a by A0, A2, PARTFUN2:def 1;

now

let x be Real; :: thesis: ( x in dom (f * (reproj 1,p)) implies (f * (reproj 1,p)) . x = a )
assume x in dom (f * (reproj 1,p)) ; :: thesis: (f * (reproj 1,p)) . x = a
then A5: (f * (reproj 1,p)) . x = f . ((reproj 1,p) . x) by FUNCT_1:22;
thus (f * (reproj 1,p)) . x = a by A3, A5; :: thesis: verum

end;

then A7: f * (reproj 1,p) is constant by PARTFUN2:def 1;
set g1 = f * (reproj 1,p);
A8: dom (f * (reproj 1,p)) = W by A0, FUNCT_2:def 1;
A9: (f * (reproj 1,p)) | W is constant by A7;
A10: f * (reproj 1,p) is_differentiable_on REAL by A8, A9, FDIFF_1:30;
A12: for x being Real st x in REAL holds
diff (f * (reproj 1,p)),x = 0

proof

let x be Real; :: thesis: ( x in REAL implies diff (f * (reproj 1,p)),x = 0 )
assume x in REAL ; :: thesis: diff (f * (reproj 1,p)),x = 0
diff (f * (reproj 1,p)),x = ((f * (reproj 1,p)) `| W) . x by A10, FDIFF_1:def 8
.= 0 by A8, A9, FDIFF_1:30 ;
hence diff (f * (reproj 1,p)),x = 0 ; :: thesis: verum

end;

A14: partdiff f,p,1 = 0 by A12;

now

let y be Real; :: thesis: ( y in dom (f * (reproj 2,p)) implies (f * (reproj 2,p)) . y = a )
assume y in dom (f * (reproj 2,p)) ; :: thesis: (f * (reproj 2,p)) . y = a
then (f * (reproj 2,p)) . y = f . ((reproj 2,p) . y) by FUNCT_1:22;
hence (f * (reproj 2,p)) . y = a by A3; :: thesis: verum

end;

then A18: f * (reproj 2,p) is constant by PARTFUN2:def 1;
set g2 = f * (reproj 2,p);
A19: dom (f * (reproj 2,p)) = W by A0, FUNCT_2:def 1;
A20: (f * (reproj 2,p)) | W is constant by A18;
A21: ( f * (reproj 2,p) is_differentiable_on REAL & ( for y being Real st y in REAL holds
((f * (reproj 2,p)) `| W) . y = 0 ) ) by A19, A20, FDIFF_1:30;
A23: for y being Real st y in REAL holds
diff (f * (reproj 2,p)),y = 0

proof

let y be Real; :: thesis: ( y in REAL implies diff (f * (reproj 2,p)),y = 0 )
assume y in REAL ; :: thesis: diff (f * (reproj 2,p)),y = 0
diff (f * (reproj 2,p)),y = ((f * (reproj 2,p)) `| W) . y by A21, FDIFF_1:def 8
.= 0 by A19, A20, FDIFF_1:30 ;
hence diff (f * (reproj 2,p)),y = 0 ; :: thesis: verum

end;

A25: partdiff f,p,2 = 0 by A23;

now

let z be Real; :: thesis: ( z in dom (f * (reproj 3,p)) implies (f * (reproj 3,p)) . z = a )
assume z in dom (f * (reproj 3,p)) ; :: thesis: (f * (reproj 3,p)) . z = a
then A27: (f * (reproj 3,p)) . z = f . ((reproj 3,p) . z) by FUNCT_1:22;
thus (f * (reproj 3,p)) . z = a by A3, A27; :: thesis: verum

end;

then A29: f * (reproj 3,p) is constant by PARTFUN2:def 1;
set g3 = f * (reproj 3,p);
A30: dom (f * (reproj 3,p)) = W by A0, FUNCT_2:def 1;
A31: (f * (reproj 3,p)) | W is constant by A29;
A32: ( f * (reproj 3,p) is_differentiable_on REAL & ( for z being Real st z in REAL holds
((f * (reproj 3,p)) `| W) . z = 0 ) ) by A30, A31, FDIFF_1:30;
A34: for z being Real st z in REAL holds
diff (f * (reproj 3,p)),z = 0

proof

let z be Real; :: thesis: ( z in REAL implies diff (f * (reproj 3,p)),z = 0 )
assume z in REAL ; :: thesis: diff (f * (reproj 3,p)),z = 0
diff (f * (reproj 3,p)),z = ((f * (reproj 3,p)) `| W) . z by A32, FDIFF_1:def 8
.= 0 by A30, A31, FDIFF_1:30 ;
hence diff (f * (reproj 3,p)),z = 0 ; :: thesis: verum

end;

A36: partdiff f,p,3 = 0 by A34;
grad f,p = |[0 ,0 ,0 ]| by A14, A25, A36, Th43
.= 0.REAL 3 by FINSEQ_2:76 ;
hence grad f,p = 0.REAL 3 ; :: thesis: verum