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
then A2: dom f = REAL 3 by 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 (f * (reproj (1,p))) . x = f . ((reproj (1,p)) . x) by FUNCT_1:22;
hence (f * (reproj (1,p))) . x = a by A3; :: 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;
then A10: f * (reproj (1,p)) is_differentiable_on REAL by A8, FDIFF_1:30;
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;

then A14: partdiff (f,p,1) = 0 ;

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;
then 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, FDIFF_1:30;
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;

then A25: partdiff (f,p,2) = 0 ;

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 (f * (reproj (3,p))) . z = f . ((reproj (3,p)) . z) by FUNCT_1:22;
hence (f * (reproj (3,p))) . z = a by A3; :: 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;
then 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, FDIFF_1:30;
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;

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