:: PDIFF_4 semantic presentation

begin


theorem Th1: :: PDIFF_4:1
( dom (proj (1,3)) = REAL 3 & rng (proj (1,3)) = REAL & ( for x, y, z being Element of REAL holds (proj (1,3)) . <*x,y,z*> = x ) )
proof
set f = proj (1,3);
A1: for x being set st x in REAL holds
ex u being set st
( u in REAL 3 & x = (proj (1,3)) . u )
proof
let x be set ; ::_thesis: ( x in REAL implies ex u being set st
( u in REAL 3 & x = (proj (1,3)) . u ) )
assume  x in REAL ; ::_thesis: ex u being set st
( u in REAL 3 & x = (proj (1,3)) . u )
then reconsider x1 = x as Element of REAL ;
set y = the Element of REAL ;
reconsider u = <*x1, the Element of REAL , the Element of REAL *> as Element of REAL 3 by FINSEQ_2:104;
 (proj (1,3)) . u = u . 1 by PDIFF_1:def_1;
then  (proj (1,3)) . u = x by FINSEQ_1:45;
hence  ex u being set st
( u in REAL 3 & x = (proj (1,3)) . u ) ; ::_thesis: verum
end;
now__::_thesis:_for_x,_y,_z_being_Element_of_REAL_holds_(proj_(1,3))_._<*x,y,z*>_=_x
let x, y, z be Element of REAL ; ::_thesis: (proj (1,3)) . <*x,y,z*> = x
 <*x,y,z*> is Element of 3 -tuples_on REAL by FINSEQ_2:104;
then  (proj (1,3)) . <*x,y,z*> = <*x,y,z*> . 1 by PDIFF_1:def_1;
hence  (proj (1,3)) . <*x,y,z*> = x by FINSEQ_1:45; ::_thesis: verum
end;
hence  ( dom (proj (1,3)) = REAL 3 & rng (proj (1,3)) = REAL & ( for x, y, z being Element of REAL holds (proj (1,3)) . <*x,y,z*> = x ) ) by A1, FUNCT_2:10, FUNCT_2:def_1; ::_thesis: verum
end;

theorem Th2: :: PDIFF_4:2
( dom (proj (2,3)) = REAL 3 & rng (proj (2,3)) = REAL & ( for x, y, z being Element of REAL holds (proj (2,3)) . <*x,y,z*> = y ) )
proof
set f = proj (2,3);
A1: for y being set st y in REAL holds
ex u being set st
( u in REAL 3 & y = (proj (2,3)) . u )
proof
let y be set ; ::_thesis: ( y in REAL implies ex u being set st
( u in REAL 3 & y = (proj (2,3)) . u ) )
assume  y in REAL ; ::_thesis: ex u being set st
( u in REAL 3 & y = (proj (2,3)) . u )
then reconsider y1 = y as Element of REAL ;
set x = the Element of REAL ;
reconsider u = <* the Element of REAL ,y1, the Element of REAL *> as Element of REAL 3 by FINSEQ_2:104;
 (proj (2,3)) . u = u . 2 by PDIFF_1:def_1;
then  (proj (2,3)) . u = y by FINSEQ_1:45;
hence  ex u being set st
( u in REAL 3 & y = (proj (2,3)) . u ) ; ::_thesis: verum
end;
now__::_thesis:_for_x,_y,_z_being_Element_of_REAL_holds_(proj_(2,3))_._<*x,y,z*>_=_y
let x, y, z be Element of REAL ; ::_thesis: (proj (2,3)) . <*x,y,z*> = y
 <*x,y,z*> is Element of 3 -tuples_on REAL by FINSEQ_2:104;
then  (proj (2,3)) . <*x,y,z*> = <*x,y,z*> . 2 by PDIFF_1:def_1;
hence  (proj (2,3)) . <*x,y,z*> = y by FINSEQ_1:45; ::_thesis: verum
end;
hence  ( dom (proj (2,3)) = REAL 3 & rng (proj (2,3)) = REAL & ( for x, y, z being Element of REAL holds (proj (2,3)) . <*x,y,z*> = y ) ) by A1, FUNCT_2:10, FUNCT_2:def_1; ::_thesis: verum
end;

theorem Th3: :: PDIFF_4:3
( dom (proj (3,3)) = REAL 3 & rng (proj (3,3)) = REAL & ( for x, y, z being Element of REAL holds (proj (3,3)) . <*x,y,z*> = z ) )
proof
set f = proj (3,3);
A1: for z being set st z in REAL holds
ex u being set st
( u in REAL 3 & z = (proj (3,3)) . u )
proof
let z be set ; ::_thesis: ( z in REAL implies ex u being set st
( u in REAL 3 & z = (proj (3,3)) . u ) )
assume  z in REAL ; ::_thesis: ex u being set st
( u in REAL 3 & z = (proj (3,3)) . u )
then reconsider z1 = z as Element of REAL ;
set x = the Element of REAL ;
reconsider u = <* the Element of REAL , the Element of REAL ,z1*> as Element of REAL 3 by FINSEQ_2:104;
 (proj (3,3)) . u = u . 3 by PDIFF_1:def_1;
then  (proj (3,3)) . u = z by FINSEQ_1:45;
hence  ex u being set st
( u in REAL 3 & z = (proj (3,3)) . u ) ; ::_thesis: verum
end;
now__::_thesis:_for_x,_y,_z_being_Element_of_REAL_holds_(proj_(3,3))_._<*x,y,z*>_=_z
let x, y, z be Element of REAL ; ::_thesis: (proj (3,3)) . <*x,y,z*> = z
 <*x,y,z*> is Element of 3 -tuples_on REAL by FINSEQ_2:104;
then  (proj (3,3)) . <*x,y,z*> = <*x,y,z*> . 3 by PDIFF_1:def_1;
hence  (proj (3,3)) . <*x,y,z*> = z by FINSEQ_1:45; ::_thesis: verum
end;
hence  ( dom (proj (3,3)) = REAL 3 & rng (proj (3,3)) = REAL & ( for x, y, z being Element of REAL holds (proj (3,3)) . <*x,y,z*> = z ) ) by A1, FUNCT_2:10, FUNCT_2:def_1; ::_thesis: verum
end;

begin

theorem Th4: :: PDIFF_4:4
for x, y, z being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,1 holds
SVF1 (1,f,u) is_differentiable_in x
proof
let x, y, z be Real; ::_thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,1 holds
SVF1 (1,f,u) is_differentiable_in x
let u be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,1 holds
SVF1 (1,f,u) is_differentiable_in x
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( u = <*x,y,z*> & f is_partial_differentiable_in u,1 implies SVF1 (1,f,u) is_differentiable_in x )
assume that
A1: u = <*x,y,z*> and
A2: f is_partial_differentiable_in u,1 ; ::_thesis: SVF1 (1,f,u) is_differentiable_in x
 (proj (1,3)) . u = x by A1, Th1;
hence  SVF1 (1,f,u) is_differentiable_in x by A2, PDIFF_1:def_11; ::_thesis: verum
end;

theorem Th5: :: PDIFF_4:5
for x, y, z being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,2 holds
SVF1 (2,f,u) is_differentiable_in y
proof
let x, y, z be Real; ::_thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,2 holds
SVF1 (2,f,u) is_differentiable_in y
let u be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,2 holds
SVF1 (2,f,u) is_differentiable_in y
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( u = <*x,y,z*> & f is_partial_differentiable_in u,2 implies SVF1 (2,f,u) is_differentiable_in y )
assume that
A1: u = <*x,y,z*> and
A2: f is_partial_differentiable_in u,2 ; ::_thesis: SVF1 (2,f,u) is_differentiable_in y
 (proj (2,3)) . u = y by A1, Th2;
hence  SVF1 (2,f,u) is_differentiable_in y by A2, PDIFF_1:def_11; ::_thesis: verum
end;

theorem Th6: :: PDIFF_4:6
for x, y, z being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,3 holds
SVF1 (3,f,u) is_differentiable_in z
proof
let x, y, z be Real; ::_thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,3 holds
SVF1 (3,f,u) is_differentiable_in z
let u be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,3 holds
SVF1 (3,f,u) is_differentiable_in z
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( u = <*x,y,z*> & f is_partial_differentiable_in u,3 implies SVF1 (3,f,u) is_differentiable_in z )
assume that
A1: u = <*x,y,z*> and
A2: f is_partial_differentiable_in u,3 ; ::_thesis: SVF1 (3,f,u) is_differentiable_in z
 (proj (3,3)) . u = z by A1, Th3;
hence  SVF1 (3,f,u) is_differentiable_in z by A2, PDIFF_1:def_11; ::_thesis: verum
end;

theorem Th7: :: PDIFF_4:7
for f being PartFunc of (REAL 3),REAL
for u being Element of REAL 3 holds
( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (1,f,u) is_differentiable_in x0 ) iff f is_partial_differentiable_in u,1 )
proof
let f be PartFunc of (REAL 3),REAL; ::_thesis: for u being Element of REAL 3 holds
( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (1,f,u) is_differentiable_in x0 ) iff f is_partial_differentiable_in u,1 )
let u be Element of REAL 3; ::_thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (1,f,u) is_differentiable_in x0 ) iff f is_partial_differentiable_in u,1 )
hereby  ::_thesis: ( f is_partial_differentiable_in u,1 implies ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (1,f,u) is_differentiable_in x0 ) )
given x0, y0, z0 being Real such that A1: ( u = <*x0,y0,z0*> & SVF1 (1,f,u) is_differentiable_in x0 ) ; ::_thesis: f is_partial_differentiable_in u,1
 (proj (1,3)) . u = x0 by A1, Th1;
hence  f is_partial_differentiable_in u,1 by A1, PDIFF_1:def_11; ::_thesis: verum
end;
assume A2: f is_partial_differentiable_in u,1 ; ::_thesis: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (1,f,u) is_differentiable_in x0 )
consider x0, y0, z0 being Real such that
A3: u = <*x0,y0,z0*> by FINSEQ_2:103;
 (proj (1,3)) . u = x0 by A3, Th1;
then  SVF1 (1,f,u) is_differentiable_in x0 by A2, PDIFF_1:def_11;
hence  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (1,f,u) is_differentiable_in x0 ) by A3; ::_thesis: verum
end;

theorem Th8: :: PDIFF_4:8
for f being PartFunc of (REAL 3),REAL
for u being Element of REAL 3 holds
( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (2,f,u) is_differentiable_in y0 ) iff f is_partial_differentiable_in u,2 )
proof
let f be PartFunc of (REAL 3),REAL; ::_thesis: for u being Element of REAL 3 holds
( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (2,f,u) is_differentiable_in y0 ) iff f is_partial_differentiable_in u,2 )
let u be Element of REAL 3; ::_thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (2,f,u) is_differentiable_in y0 ) iff f is_partial_differentiable_in u,2 )
hereby  ::_thesis: ( f is_partial_differentiable_in u,2 implies ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (2,f,u) is_differentiable_in y0 ) )
given x0, y0, z0 being Real such that A1: ( u = <*x0,y0,z0*> & SVF1 (2,f,u) is_differentiable_in y0 ) ; ::_thesis: f is_partial_differentiable_in u,2
 (proj (2,3)) . u = y0 by A1, Th2;
hence  f is_partial_differentiable_in u,2 by A1, PDIFF_1:def_11; ::_thesis: verum
end;
assume A2: f is_partial_differentiable_in u,2 ; ::_thesis: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (2,f,u) is_differentiable_in y0 )
consider x0, y0, z0 being Real such that
A3: u = <*x0,y0,z0*> by FINSEQ_2:103;
 (proj (2,3)) . u = y0 by A3, Th2;
then  SVF1 (2,f,u) is_differentiable_in y0 by A2, PDIFF_1:def_11;
hence  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (2,f,u) is_differentiable_in y0 ) by A3; ::_thesis: verum
end;

theorem Th9: :: PDIFF_4:9
for f being PartFunc of (REAL 3),REAL
for u being Element of REAL 3 holds
( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (3,f,u) is_differentiable_in z0 ) iff f is_partial_differentiable_in u,3 )
proof
let f be PartFunc of (REAL 3),REAL; ::_thesis: for u being Element of REAL 3 holds
( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (3,f,u) is_differentiable_in z0 ) iff f is_partial_differentiable_in u,3 )
let u be Element of REAL 3; ::_thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (3,f,u) is_differentiable_in z0 ) iff f is_partial_differentiable_in u,3 )
hereby  ::_thesis: ( f is_partial_differentiable_in u,3 implies ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (3,f,u) is_differentiable_in z0 ) )
given x0, y0, z0 being Real such that A1: ( u = <*x0,y0,z0*> & SVF1 (3,f,u) is_differentiable_in z0 ) ; ::_thesis: f is_partial_differentiable_in u,3
 (proj (3,3)) . u = z0 by A1, Th3;
hence  f is_partial_differentiable_in u,3 by A1, PDIFF_1:def_11; ::_thesis: verum
end;
assume A2: f is_partial_differentiable_in u,3 ; ::_thesis: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (3,f,u) is_differentiable_in z0 )
consider x0, y0, z0 being Real such that
A3: u = <*x0,y0,z0*> by FINSEQ_2:103;
 (proj (3,3)) . u = z0 by A3, Th3;
then  SVF1 (3,f,u) is_differentiable_in z0 by A2, PDIFF_1:def_11;
hence  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 (3,f,u) is_differentiable_in z0 ) by A3; ::_thesis: verum
end;

theorem :: PDIFF_4:10
for x0, y0, z0 being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
proof
let x0, y0, z0 be Real; ::_thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
let u be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 implies ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) )
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_partial_differentiable_in u,1 ; ::_thesis: ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
consider x1, y1, z1 being Real such that
A3: ( u = <*x1,y1,z1*> & SVF1 (1,f,u) is_differentiable_in x1 ) by A2, Th7;
 SVF1 (1,f,u) is_differentiable_in x0 by A1, A3, FINSEQ_1:78;
hence  ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by FDIFF_1:def_4; ::_thesis: verum
end;

theorem :: PDIFF_4:11
for x0, y0, z0 being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
proof
let x0, y0, z0 be Real; ::_thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
let u be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 implies ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) )
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_partial_differentiable_in u,2 ; ::_thesis: ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
consider x1, y1, z1 being Real such that
A3: ( u = <*x1,y1,z1*> & SVF1 (2,f,u) is_differentiable_in y1 ) by A2, Th8;
 SVF1 (2,f,u) is_differentiable_in y0 by A1, A3, FINSEQ_1:78;
hence  ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by FDIFF_1:def_4; ::_thesis: verum
end;

theorem :: PDIFF_4:12
for x0, y0, z0 being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) )
proof
let x0, y0, z0 be Real; ::_thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) )
let u be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) )
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 implies ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) )
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_partial_differentiable_in u,3 ; ::_thesis: ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) )
consider x1, y1, z1 being Real such that
A3: ( u = <*x1,y1,z1*> & SVF1 (3,f,u) is_differentiable_in z1 ) by A2, Th9;
 SVF1 (3,f,u) is_differentiable_in z0 by A1, A3, FINSEQ_1:78;
hence  ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) by FDIFF_1:def_4; ::_thesis: verum
end;

theorem Th13: :: PDIFF_4:13
for f being PartFunc of (REAL 3),REAL
for u being Element of REAL 3 holds
( f is_partial_differentiable_in u,1 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
proof
let f be PartFunc of (REAL 3),REAL; ::_thesis: for u being Element of REAL 3 holds
( f is_partial_differentiable_in u,1 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
let u be Element of REAL 3; ::_thesis: ( f is_partial_differentiable_in u,1 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
hereby  ::_thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) implies f is_partial_differentiable_in u,1 )
assume A1: f is_partial_differentiable_in u,1 ; ::_thesis: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) )
thus  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ::_thesis: verum
proof
consider x0, y0, z0 being Real such that
A2: ( u = <*x0,y0,z0*> & SVF1 (1,f,u) is_differentiable_in x0 ) by A1, Th7;
 ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A2, FDIFF_1:def_4;
hence  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A2; ::_thesis: verum
end;
end;
assume  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ; ::_thesis: f is_partial_differentiable_in u,1
then consider x0, y0, z0 being Real such that
A3: ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ;
consider N being Neighbourhood of x0 such that
A4: ( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A3;
 SVF1 (1,f,u) is_differentiable_in x0 by A4, FDIFF_1:def_4;
hence  f is_partial_differentiable_in u,1 by A3, Th7; ::_thesis: verum
end;

theorem Th14: :: PDIFF_4:14
for f being PartFunc of (REAL 3),REAL
for u being Element of REAL 3 holds
( f is_partial_differentiable_in u,2 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )
proof
let f be PartFunc of (REAL 3),REAL; ::_thesis: for u being Element of REAL 3 holds
( f is_partial_differentiable_in u,2 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )
let u be Element of REAL 3; ::_thesis: ( f is_partial_differentiable_in u,2 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )
hereby  ::_thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) implies f is_partial_differentiable_in u,2 )
assume A1: f is_partial_differentiable_in u,2 ; ::_thesis: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) )
thus  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ::_thesis: verum
proof
consider x0, y0, z0 being Real such that
A2: ( u = <*x0,y0,z0*> & SVF1 (2,f,u) is_differentiable_in y0 ) by A1, Th8;
 ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A2, FDIFF_1:def_4;
hence  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by A2; ::_thesis: verum
end;
end;
assume  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ; ::_thesis: f is_partial_differentiable_in u,2
then consider x0, y0, z0 being Real such that
A3: ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ;
consider N being Neighbourhood of y0 such that
A4: ( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A3;
 SVF1 (2,f,u) is_differentiable_in y0 by A4, FDIFF_1:def_4;
hence  f is_partial_differentiable_in u,2 by A3, Th8; ::_thesis: verum
end;

theorem Th15: :: PDIFF_4:15
for f being PartFunc of (REAL 3),REAL
for u being Element of REAL 3 holds
( f is_partial_differentiable_in u,3 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) )
proof
let f be PartFunc of (REAL 3),REAL; ::_thesis: for u being Element of REAL 3 holds
( f is_partial_differentiable_in u,3 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) )
let u be Element of REAL 3; ::_thesis: ( f is_partial_differentiable_in u,3 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) )
hereby  ::_thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) implies f is_partial_differentiable_in u,3 )
assume A1: f is_partial_differentiable_in u,3 ; ::_thesis: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) )
thus  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ::_thesis: verum
proof
consider x0, y0, z0 being Real such that
A2: ( u = <*x0,y0,z0*> & SVF1 (3,f,u) is_differentiable_in z0 ) by A1, Th9;
 ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) by A2, FDIFF_1:def_4;
hence  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) by A2; ::_thesis: verum
end;
end;
assume  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ; ::_thesis: f is_partial_differentiable_in u,3
then consider x0, y0, z0 being Real such that
A3: ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ;
consider N being Neighbourhood of z0 such that
A4: ( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) by A3;
 SVF1 (3,f,u) is_differentiable_in z0 by A4, FDIFF_1:def_4;
hence  f is_partial_differentiable_in u,3 by A3, Th9; ::_thesis: verum
end;

Lm1:  for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
( r = diff ((SVF1 (1,f,u)),x0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
proof
let x0, y0, z0, r be Real; ::_thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
( r = diff ((SVF1 (1,f,u)),x0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
let u be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
( r = diff ((SVF1 (1,f,u)),x0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 implies ( r = diff ((SVF1 (1,f,u)),x0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ) )
set F1 = SVF1 (1,f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_partial_differentiable_in u,1 ; ::_thesis: ( r = diff ((SVF1 (1,f,u)),x0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
hereby  ::_thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) implies r = diff ((SVF1 (1,f,u)),x0) )
assume A3: r = diff ((SVF1 (1,f,u)),x0) ; ::_thesis: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
 SVF1 (1,f,u) is_differentiable_in x0 by A1, A2, Th4;
then consider N being Neighbourhood of x0 such that
A4: ( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) by A3, FDIFF_1:def_5;
thus  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) by A1, A4; ::_thesis: verum
end;
given x1, y1, z1 being Real such that A5: ( u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) ) ) ; ::_thesis: r = diff ((SVF1 (1,f,u)),x0)
A6: x1 = x0 by A5, A1, FINSEQ_1:78;
 SVF1 (1,f,u) is_differentiable_in x0 by A1, A2, Th4;
hence  r = diff ((SVF1 (1,f,u)),x0) by A6, A5, FDIFF_1:def_5; ::_thesis: verum
end;

Lm2:  for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
( r = diff ((SVF1 (2,f,u)),y0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
proof
let x0, y0, z0, r be Real; ::_thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
( r = diff ((SVF1 (2,f,u)),y0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
let u be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
( r = diff ((SVF1 (2,f,u)),y0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 implies ( r = diff ((SVF1 (2,f,u)),y0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ) )
set F1 = SVF1 (2,f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_partial_differentiable_in u,2 ; ::_thesis: ( r = diff ((SVF1 (2,f,u)),y0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
hereby  ::_thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) implies r = diff ((SVF1 (2,f,u)),y0) )
assume A3: r = diff ((SVF1 (2,f,u)),y0) ; ::_thesis: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
 SVF1 (2,f,u) is_differentiable_in y0 by A1, A2, Th5;
then consider N being Neighbourhood of y0 such that
A4: ( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) by A3, FDIFF_1:def_5;
thus  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) by A1, A4; ::_thesis: verum
end;
given x1, y1, z1 being Real such that A5: ( u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) ) ) ; ::_thesis: r = diff ((SVF1 (2,f,u)),y0)
A6: y1 = y0 by A5, A1, FINSEQ_1:78;
 SVF1 (2,f,u) is_differentiable_in y0 by A1, A2, Th5;
hence  r = diff ((SVF1 (2,f,u)),y0) by A6, A5, FDIFF_1:def_5; ::_thesis: verum
end;

Lm3:  for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
( r = diff ((SVF1 (3,f,u)),z0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )
proof
let x0, y0, z0, r be Real; ::_thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
( r = diff ((SVF1 (3,f,u)),z0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )
let u be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
( r = diff ((SVF1 (3,f,u)),z0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 implies ( r = diff ((SVF1 (3,f,u)),z0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) ) )
set F1 = SVF1 (3,f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_partial_differentiable_in u,3 ; ::_thesis: ( r = diff ((SVF1 (3,f,u)),z0) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )
hereby  ::_thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) implies r = diff ((SVF1 (3,f,u)),z0) )
assume A3: r = diff ((SVF1 (3,f,u)),z0) ; ::_thesis: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) )
 SVF1 (3,f,u) is_differentiable_in z0 by A1, A2, Th6;
then consider N being Neighbourhood of z0 such that
A4: ( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) by A3, FDIFF_1:def_5;
thus  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) by A1, A4; ::_thesis: verum
end;
given x1, y1, z1 being Real such that A5: ( u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z1) = (L . (z - z1)) + (R . (z - z1)) ) ) ) ) ; ::_thesis: r = diff ((SVF1 (3,f,u)),z0)
A6: z1 = z0 by A5, A1, FINSEQ_1:78;
 SVF1 (3,f,u) is_differentiable_in z0 by A1, A2, Th6;
hence  r = diff ((SVF1 (3,f,u)),z0) by A6, A5, FDIFF_1:def_5; ::_thesis: verum
end;

theorem Th16: :: PDIFF_4:16
for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
( r = partdiff (f,u,1) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
proof
let x0, y0, z0, r be Real; ::_thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
( r = partdiff (f,u,1) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
let u be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
( r = partdiff (f,u,1) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 implies ( r = partdiff (f,u,1) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ) )
assume A1: ( u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 ) ; ::_thesis: ( r = partdiff (f,u,1) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
hereby  ::_thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) implies r = partdiff (f,u,1) )
assume  r = partdiff (f,u,1) ; ::_thesis: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
then  r = diff ((SVF1 (1,f,u)),x0) by Th1, A1;
hence  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) by Lm1, A1; ::_thesis: verum
end;
given x1, y1, z1 being Real such that A2: ( u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) ) ) ; ::_thesis: r = partdiff (f,u,1)
 r = diff ((SVF1 (1,f,u)),x0) by A2, A1, Lm1;
hence  r = partdiff (f,u,1) by Th1, A1; ::_thesis: verum
end;

theorem Th17: :: PDIFF_4:17
for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
( r = partdiff (f,u,2) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
proof
let x0, y0, z0, r be Real; ::_thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
( r = partdiff (f,u,2) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
let u be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
( r = partdiff (f,u,2) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 implies ( r = partdiff (f,u,2) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ) )
assume A1: ( u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 ) ; ::_thesis: ( r = partdiff (f,u,2) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
hereby  ::_thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) implies r = partdiff (f,u,2) )
assume  r = partdiff (f,u,2) ; ::_thesis: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
then  r = diff ((SVF1 (2,f,u)),y0) by Th2, A1;
hence  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) by Lm2, A1; ::_thesis: verum
end;
given x1, y1, z1 being Real such that A2: ( u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) ) ) ; ::_thesis: r = partdiff (f,u,2)
 r = diff ((SVF1 (2,f,u)),y0) by A2, A1, Lm2;
hence  r = partdiff (f,u,2) by Th2, A1; ::_thesis: verum
end;

theorem Th18: :: PDIFF_4:18
for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
( r = partdiff (f,u,3) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )
proof
let x0, y0, z0, r be Real; ::_thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
( r = partdiff (f,u,3) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )
let u be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
( r = partdiff (f,u,3) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 implies ( r = partdiff (f,u,3) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) ) )
assume A1: ( u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 ) ; ::_thesis: ( r = partdiff (f,u,3) iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )
hereby  ::_thesis: ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) implies r = partdiff (f,u,3) )
assume  r = partdiff (f,u,3) ; ::_thesis: ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) )
then  r = diff ((SVF1 (3,f,u)),z0) by Th3, A1;
hence  ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) by Lm3, A1; ::_thesis: verum
end;
given x1, y1, z1 being Real such that A2: ( u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z1) = (L . (z - z1)) + (R . (z - z1)) ) ) ) ) ; ::_thesis: r = partdiff (f,u,3)
 r = diff ((SVF1 (3,f,u)),z0) by A2, A1, Lm3;
hence  r = partdiff (f,u,3) by Th3, A1; ::_thesis: verum
end;

theorem :: PDIFF_4:19
for x0, y0, z0 being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> holds
partdiff (f,u,1) = diff ((SVF1 (1,f,u)),x0) by Th1;

theorem :: PDIFF_4:20
for x0, y0, z0 being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> holds
partdiff (f,u,2) = diff ((SVF1 (2,f,u)),y0) by Th2;

theorem :: PDIFF_4:21
for x0, y0, z0 being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> holds
partdiff (f,u,3) = diff ((SVF1 (3,f,u)),z0) by Th3;

definition
let f be PartFunc of (REAL 3),REAL;
let D be set ;
predf is_partial_differentiable`1_on D means :Def1: :: PDIFF_4:def 1
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,1 ) );
predf is_partial_differentiable`2_on D means :Def2: :: PDIFF_4:def 2
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,2 ) );
predf is_partial_differentiable`3_on D means :Def3: :: PDIFF_4:def 3
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,3 ) );
end;

:: deftheorem Def1 defines is_partial_differentiable`1_on PDIFF_4:def_1_:_
 for f being PartFunc of (REAL 3),REAL
for D being set holds
( f is_partial_differentiable`1_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,1 ) ) );

:: deftheorem Def2 defines is_partial_differentiable`2_on PDIFF_4:def_2_:_
 for f being PartFunc of (REAL 3),REAL
for D being set holds
( f is_partial_differentiable`2_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,2 ) ) );

:: deftheorem Def3 defines is_partial_differentiable`3_on PDIFF_4:def_3_:_
 for f being PartFunc of (REAL 3),REAL
for D being set holds
( f is_partial_differentiable`3_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,3 ) ) );

theorem :: PDIFF_4:22
for D being set
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`1_on D holds
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,1 ) )
proof
let D be set ; ::_thesis: for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`1_on D holds
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,1 ) )
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( f is_partial_differentiable`1_on D implies ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,1 ) ) )
assume A1: f is_partial_differentiable`1_on D ; ::_thesis: ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,1 ) )
hence  D c= dom f by Def1; ::_thesis: for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,1
set g = f | D;
let u0 be Element of REAL 3; ::_thesis: ( u0 in D implies f is_partial_differentiable_in u0,1 )
assume  u0 in D ; ::_thesis: f is_partial_differentiable_in u0,1
then  f | D is_partial_differentiable_in u0,1 by A1, Def1;
then consider x0, y0, z0 being Real such that
A2: ( u0 = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(f | D),u0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(f | D),u0)) . x) - ((SVF1 (1,(f | D),u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by Th13;
consider N being Neighbourhood of x0 such that
A3: ( N c= dom (SVF1 (1,(f | D),u0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(f | D),u0)) . x) - ((SVF1 (1,(f | D),u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A2;
 for x being Real st x in dom (SVF1 (1,(f | D),u0)) holds
x in dom (SVF1 (1,f,u0))
proof
let x be Real; ::_thesis: ( x in dom (SVF1 (1,(f | D),u0)) implies x in dom (SVF1 (1,f,u0)) )
assume  x in dom (SVF1 (1,(f | D),u0)) ; ::_thesis: x in dom (SVF1 (1,f,u0))
then A4: ( x in dom (reproj (1,u0)) & (reproj (1,u0)) . x in dom (f | D) ) by FUNCT_1:11;
 dom (f | D) = (dom f) /\ D by RELAT_1:61;
then  dom (f | D) c= dom f by XBOOLE_1:17;
hence  x in dom (SVF1 (1,f,u0)) by A4, FUNCT_1:11; ::_thesis: verum
end;
then  for x being set st x in dom (SVF1 (1,(f | D),u0)) holds
x in dom (SVF1 (1,f,u0)) ;
then  dom (SVF1 (1,(f | D),u0)) c= dom (SVF1 (1,f,u0)) by TARSKI:def_3;
then A5: N c= dom (SVF1 (1,f,u0)) by A3, XBOOLE_1:1;
consider L being LinearFunc, R being RestFunc such that
A6: for x being Real st x in N holds
((SVF1 (1,(f | D),u0)) . x) - ((SVF1 (1,(f | D),u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3;
 for x being Real st x in N holds
((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) = (L . (x - x0)) + (R . (x - x0))
proof
let x be Real; ::_thesis: ( x in N implies ((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A7: x in N ; ::_thesis: ((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) = (L . (x - x0)) + (R . (x - x0))
A8: for x being Real st x in dom (SVF1 (1,(f | D),u0)) holds
(SVF1 (1,(f | D),u0)) . x = (SVF1 (1,f,u0)) . x
proof
let x be Real; ::_thesis: ( x in dom (SVF1 (1,(f | D),u0)) implies (SVF1 (1,(f | D),u0)) . x = (SVF1 (1,f,u0)) . x )
assume A9: x in dom (SVF1 (1,(f | D),u0)) ; ::_thesis: (SVF1 (1,(f | D),u0)) . x = (SVF1 (1,f,u0)) . x
then A10: ( x in dom (reproj (1,u0)) & (reproj (1,u0)) . x in dom (f | D) ) by FUNCT_1:11;
(SVF1 (1,(f | D),u0)) . x = (f | D) . ((reproj (1,u0)) . x) by A9, FUNCT_1:12
.= f . ((reproj (1,u0)) . x) by A10, FUNCT_1:47
.= (SVF1 (1,f,u0)) . x by A10, FUNCT_1:13 ;
hence  (SVF1 (1,(f | D),u0)) . x = (SVF1 (1,f,u0)) . x ; ::_thesis: verum
end;
A11: x0 in N by RCOMP_1:16;
(L . (x - x0)) + (R . (x - x0)) = ((SVF1 (1,(f | D),u0)) . x) - ((SVF1 (1,(f | D),u0)) . x0) by A6, A7
.= ((SVF1 (1,f,u0)) . x) - ((SVF1 (1,(f | D),u0)) . x0) by A3, A7, A8
.= ((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) by A3, A8, A11 ;
hence  ((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ; ::_thesis: verum
end;
hence  f is_partial_differentiable_in u0,1 by A2, A5, Th13; ::_thesis: verum
end;

theorem :: PDIFF_4:23
for D being set
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`2_on D holds
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,2 ) )
proof
let D be set ; ::_thesis: for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`2_on D holds
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,2 ) )
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( f is_partial_differentiable`2_on D implies ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,2 ) ) )
assume A1: f is_partial_differentiable`2_on D ; ::_thesis: ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,2 ) )
hence  D c= dom f by Def2; ::_thesis: for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,2
set g = f | D;
let u0 be Element of REAL 3; ::_thesis: ( u0 in D implies f is_partial_differentiable_in u0,2 )
assume  u0 in D ; ::_thesis: f is_partial_differentiable_in u0,2
then  f | D is_partial_differentiable_in u0,2 by A1, Def2;
then consider x0, y0, z0 being Real such that
A2: ( u0 = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(f | D),u0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(f | D),u0)) . y) - ((SVF1 (2,(f | D),u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by Th14;
consider N being Neighbourhood of y0 such that
A3: ( N c= dom (SVF1 (2,(f | D),u0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(f | D),u0)) . y) - ((SVF1 (2,(f | D),u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A2;
 for y being Real st y in dom (SVF1 (2,(f | D),u0)) holds
y in dom (SVF1 (2,f,u0))
proof
let y be Real; ::_thesis: ( y in dom (SVF1 (2,(f | D),u0)) implies y in dom (SVF1 (2,f,u0)) )
assume  y in dom (SVF1 (2,(f | D),u0)) ; ::_thesis: y in dom (SVF1 (2,f,u0))
then A4: ( y in dom (reproj (2,u0)) & (reproj (2,u0)) . y in dom (f | D) ) by FUNCT_1:11;
 dom (f | D) = (dom f) /\ D by RELAT_1:61;
then  dom (f | D) c= dom f by XBOOLE_1:17;
hence  y in dom (SVF1 (2,f,u0)) by A4, FUNCT_1:11; ::_thesis: verum
end;
then  for y being set st y in dom (SVF1 (2,(f | D),u0)) holds
y in dom (SVF1 (2,f,u0)) ;
then  dom (SVF1 (2,(f | D),u0)) c= dom (SVF1 (2,f,u0)) by TARSKI:def_3;
then A5: N c= dom (SVF1 (2,f,u0)) by A3, XBOOLE_1:1;
consider L being LinearFunc, R being RestFunc such that
A6: for y being Real st y in N holds
((SVF1 (2,(f | D),u0)) . y) - ((SVF1 (2,(f | D),u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A3;
 for y being Real st y in N holds
((SVF1 (2,f,u0)) . y) - ((SVF1 (2,f,u0)) . y0) = (L . (y - y0)) + (R . (y - y0))
proof
let y be Real; ::_thesis: ( y in N implies ((SVF1 (2,f,u0)) . y) - ((SVF1 (2,f,u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
assume A7: y in N ; ::_thesis: ((SVF1 (2,f,u0)) . y) - ((SVF1 (2,f,u0)) . y0) = (L . (y - y0)) + (R . (y - y0))
A8: for y being Real st y in dom (SVF1 (2,(f | D),u0)) holds
(SVF1 (2,(f | D),u0)) . y = (SVF1 (2,f,u0)) . y
proof
let y be Real; ::_thesis: ( y in dom (SVF1 (2,(f | D),u0)) implies (SVF1 (2,(f | D),u0)) . y = (SVF1 (2,f,u0)) . y )
assume A9: y in dom (SVF1 (2,(f | D),u0)) ; ::_thesis: (SVF1 (2,(f | D),u0)) . y = (SVF1 (2,f,u0)) . y
then A10: ( y in dom (reproj (2,u0)) & (reproj (2,u0)) . y in dom (f | D) ) by FUNCT_1:11;
(SVF1 (2,(f | D),u0)) . y = (f | D) . ((reproj (2,u0)) . y) by A9, FUNCT_1:12
.= f . ((reproj (2,u0)) . y) by A10, FUNCT_1:47
.= (SVF1 (2,f,u0)) . y by A10, FUNCT_1:13 ;
hence  (SVF1 (2,(f | D),u0)) . y = (SVF1 (2,f,u0)) . y ; ::_thesis: verum
end;
A11: y0 in N by RCOMP_1:16;
(L . (y - y0)) + (R . (y - y0)) = ((SVF1 (2,(f | D),u0)) . y) - ((SVF1 (2,(f | D),u0)) . y0) by A6, A7
.= ((SVF1 (2,f,u0)) . y) - ((SVF1 (2,(f | D),u0)) . y0) by A3, A7, A8
.= ((SVF1 (2,f,u0)) . y) - ((SVF1 (2,f,u0)) . y0) by A3, A8, A11 ;
hence  ((SVF1 (2,f,u0)) . y) - ((SVF1 (2,f,u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) ; ::_thesis: verum
end;
hence  f is_partial_differentiable_in u0,2 by A2, A5, Th14; ::_thesis: verum
end;

theorem :: PDIFF_4:24
for D being set
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`3_on D holds
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,3 ) )
proof
let D be set ; ::_thesis: for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`3_on D holds
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,3 ) )
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( f is_partial_differentiable`3_on D implies ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,3 ) ) )
assume A1: f is_partial_differentiable`3_on D ; ::_thesis: ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,3 ) )
hence  D c= dom f by Def3; ::_thesis: for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,3
set g = f | D;
let u0 be Element of REAL 3; ::_thesis: ( u0 in D implies f is_partial_differentiable_in u0,3 )
assume  u0 in D ; ::_thesis: f is_partial_differentiable_in u0,3
then  f | D is_partial_differentiable_in u0,3 by A1, Def3;
then consider x0, y0, z0 being Real such that
A2: ( u0 = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,(f | D),u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,(f | D),u0)) . z) - ((SVF1 (3,(f | D),u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) by Th15;
consider N being Neighbourhood of z0 such that
A3: ( N c= dom (SVF1 (3,(f | D),u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,(f | D),u0)) . z) - ((SVF1 (3,(f | D),u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) by A2;
 for z being Real st z in dom (SVF1 (3,(f | D),u0)) holds
z in dom (SVF1 (3,f,u0))
proof
let z be Real; ::_thesis: ( z in dom (SVF1 (3,(f | D),u0)) implies z in dom (SVF1 (3,f,u0)) )
assume  z in dom (SVF1 (3,(f | D),u0)) ; ::_thesis: z in dom (SVF1 (3,f,u0))
then A4: ( z in dom (reproj (3,u0)) & (reproj (3,u0)) . z in dom (f | D) ) by FUNCT_1:11;
 dom (f | D) = (dom f) /\ D by RELAT_1:61;
then  dom (f | D) c= dom f by XBOOLE_1:17;
hence  z in dom (SVF1 (3,f,u0)) by A4, FUNCT_1:11; ::_thesis: verum
end;
then  for z being set st z in dom (SVF1 (3,(f | D),u0)) holds
z in dom (SVF1 (3,f,u0)) ;
then  dom (SVF1 (3,(f | D),u0)) c= dom (SVF1 (3,f,u0)) by TARSKI:def_3;
then A5: N c= dom (SVF1 (3,f,u0)) by A3, XBOOLE_1:1;
consider L being LinearFunc, R being RestFunc such that
A6: for z being Real st z in N holds
((SVF1 (3,(f | D),u0)) . z) - ((SVF1 (3,(f | D),u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) by A3;
 for z being Real st z in N holds
((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) = (L . (z - z0)) + (R . (z - z0))
proof
let z be Real; ::_thesis: ( z in N implies ((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) )
assume A7: z in N ; ::_thesis: ((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) = (L . (z - z0)) + (R . (z - z0))
A8: for z being Real st z in dom (SVF1 (3,(f | D),u0)) holds
(SVF1 (3,(f | D),u0)) . z = (SVF1 (3,f,u0)) . z
proof
let z be Real; ::_thesis: ( z in dom (SVF1 (3,(f | D),u0)) implies (SVF1 (3,(f | D),u0)) . z = (SVF1 (3,f,u0)) . z )
assume A9: z in dom (SVF1 (3,(f | D),u0)) ; ::_thesis: (SVF1 (3,(f | D),u0)) . z = (SVF1 (3,f,u0)) . z
then A10: ( z in dom (reproj (3,u0)) & (reproj (3,u0)) . z in dom (f | D) ) by FUNCT_1:11;
(SVF1 (3,(f | D),u0)) . z = (f | D) . ((reproj (3,u0)) . z) by A9, FUNCT_1:12
.= f . ((reproj (3,u0)) . z) by A10, FUNCT_1:47
.= (SVF1 (3,f,u0)) . z by A10, FUNCT_1:13 ;
hence  (SVF1 (3,(f | D),u0)) . z = (SVF1 (3,f,u0)) . z ; ::_thesis: verum
end;
A11: z0 in N by RCOMP_1:16;
(L . (z - z0)) + (R . (z - z0)) = ((SVF1 (3,(f | D),u0)) . z) - ((SVF1 (3,(f | D),u0)) . z0) by A6, A7
.= ((SVF1 (3,f,u0)) . z) - ((SVF1 (3,(f | D),u0)) . z0) by A3, A7, A8
.= ((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) by A3, A8, A11 ;
hence  ((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) ; ::_thesis: verum
end;
hence  f is_partial_differentiable_in u0,3 by A2, A5, Th15; ::_thesis: verum
end;

definition
let f be PartFunc of (REAL 3),REAL;
let D be set ;
assume A1: f is_partial_differentiable`1_on D ;
funcf `partial1| D ->  PartFunc of (REAL 3),REAL means :: PDIFF_4:def 4
( dom it = D & ( for u being Element of REAL 3 st u in D holds
it . u = partdiff (f,u,1) ) );
existence
 ex b1 being PartFunc of (REAL 3),REAL st
( dom b1 = D & ( for u being Element of REAL 3 st u in D holds
b1 . u = partdiff (f,u,1) ) )
proof
defpred S1[ Element of REAL 3] means $1 in D;
deffunc H1( Element of REAL 3) ->  Element of REAL = partdiff (f,$1,1);
consider F being PartFunc of (REAL 3),REAL such that
A2: ( ( for u being Element of REAL 3 holds
( u in dom F iff S1[u] ) ) & ( for u being Element of REAL 3 st u in dom F holds
F . u = H1(u) ) ) from SEQ_1:sch_3();
take  F ; ::_thesis: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,1) ) )
 for y being set st y in dom F holds
y in D by A2;
then A3: dom F c= D by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_D_holds_
y_in_dom_F
let y be set ; ::_thesis: ( y in D implies y in dom F )
assume A4: y in D ; ::_thesis: y in dom F
 D c= dom f by A1, Def1;
then  D is Subset of (REAL 3) by XBOOLE_1:1;
hence  y in dom F by A2, A4; ::_thesis: verum
end;
then  D c= dom F by TARSKI:def_3;
hence  dom F = D by A3, XBOOLE_0:def_10; ::_thesis: for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,1)
let u be Element of REAL 3; ::_thesis: ( u in D implies F . u = partdiff (f,u,1) )
assume  u in D ; ::_thesis: F . u = partdiff (f,u,1)
then  u in dom F by A2;
hence  F . u = partdiff (f,u,1) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds
b1 . u = partdiff (f,u,1) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds
b2 . u = partdiff (f,u,1) ) holds
b1 = b2
proof
let F, G be PartFunc of (REAL 3),REAL; ::_thesis: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,1) ) & dom G = D & ( for u being Element of REAL 3 st u in D holds
G . u = partdiff (f,u,1) ) implies F = G )
assume that
A5: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,1) ) ) and
A6: ( dom G = D & ( for u being Element of REAL 3 st u in D holds
G . u = partdiff (f,u,1) ) ) ; ::_thesis: F = G
now__::_thesis:_for_u_being_Element_of_REAL_3_st_u_in_dom_F_holds_
F_._u_=_G_._u
let u be Element of REAL 3; ::_thesis: ( u in dom F implies F . u = G . u )
assume A7: u in dom F ; ::_thesis: F . u = G . u
then  F . u = partdiff (f,u,1) by A5;
hence  F . u = G . u by A5, A6, A7; ::_thesis: verum
end;
hence  F = G by A5, A6, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem  defines `partial1| PDIFF_4:def_4_:_
 for f being PartFunc of (REAL 3),REAL
for D being set st f is_partial_differentiable`1_on D holds
for b3 being PartFunc of (REAL 3),REAL holds
( b3 = f `partial1| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds
b3 . u = partdiff (f,u,1) ) ) );

definition
let f be PartFunc of (REAL 3),REAL;
let D be set ;
assume A1: f is_partial_differentiable`2_on D ;
funcf `partial2| D ->  PartFunc of (REAL 3),REAL means :: PDIFF_4:def 5
( dom it = D & ( for u being Element of REAL 3 st u in D holds
it . u = partdiff (f,u,2) ) );
existence
 ex b1 being PartFunc of (REAL 3),REAL st
( dom b1 = D & ( for u being Element of REAL 3 st u in D holds
b1 . u = partdiff (f,u,2) ) )
proof
defpred S1[ Element of REAL 3] means $1 in D;
deffunc H1( Element of REAL 3) ->  Element of REAL = partdiff (f,$1,2);
consider F being PartFunc of (REAL 3),REAL such that
A2: ( ( for u being Element of REAL 3 holds
( u in dom F iff S1[u] ) ) & ( for u being Element of REAL 3 st u in dom F holds
F . u = H1(u) ) ) from SEQ_1:sch_3();
take  F ; ::_thesis: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,2) ) )
 for y being set st y in dom F holds
y in D by A2;
then A3: dom F c= D by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_D_holds_
y_in_dom_F
let y be set ; ::_thesis: ( y in D implies y in dom F )
assume A4: y in D ; ::_thesis: y in dom F
 D c= dom f by A1, Def2;
then  D is Subset of (REAL 3) by XBOOLE_1:1;
hence  y in dom F by A2, A4; ::_thesis: verum
end;
then  D c= dom F by TARSKI:def_3;
hence  dom F = D by A3, XBOOLE_0:def_10; ::_thesis: for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,2)
let u be Element of REAL 3; ::_thesis: ( u in D implies F . u = partdiff (f,u,2) )
assume  u in D ; ::_thesis: F . u = partdiff (f,u,2)
then  u in dom F by A2;
hence  F . u = partdiff (f,u,2) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds
b1 . u = partdiff (f,u,2) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds
b2 . u = partdiff (f,u,2) ) holds
b1 = b2
proof
let F, G be PartFunc of (REAL 3),REAL; ::_thesis: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,2) ) & dom G = D & ( for u being Element of REAL 3 st u in D holds
G . u = partdiff (f,u,2) ) implies F = G )
assume that
A5: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,2) ) ) and
A6: ( dom G = D & ( for u being Element of REAL 3 st u in D holds
G . u = partdiff (f,u,2) ) ) ; ::_thesis: F = G
now__::_thesis:_for_u_being_Element_of_REAL_3_st_u_in_dom_F_holds_
F_._u_=_G_._u
let u be Element of REAL 3; ::_thesis: ( u in dom F implies F . u = G . u )
assume A7: u in dom F ; ::_thesis: F . u = G . u
then  F . u = partdiff (f,u,2) by A5;
hence  F . u = G . u by A5, A6, A7; ::_thesis: verum
end;
hence  F = G by A5, A6, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem  defines `partial2| PDIFF_4:def_5_:_
 for f being PartFunc of (REAL 3),REAL
for D being set st f is_partial_differentiable`2_on D holds
for b3 being PartFunc of (REAL 3),REAL holds
( b3 = f `partial2| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds
b3 . u = partdiff (f,u,2) ) ) );

definition
let f be PartFunc of (REAL 3),REAL;
let D be set ;
assume A1: f is_partial_differentiable`3_on D ;
funcf `partial3| D ->  PartFunc of (REAL 3),REAL means :: PDIFF_4:def 6
( dom it = D & ( for u being Element of REAL 3 st u in D holds
it . u = partdiff (f,u,3) ) );
existence
 ex b1 being PartFunc of (REAL 3),REAL st
( dom b1 = D & ( for u being Element of REAL 3 st u in D holds
b1 . u = partdiff (f,u,3) ) )
proof
defpred S1[ Element of REAL 3] means $1 in D;
deffunc H1( Element of REAL 3) ->  Element of REAL = partdiff (f,$1,3);
consider F being PartFunc of (REAL 3),REAL such that
A2: ( ( for u being Element of REAL 3 holds
( u in dom F iff S1[u] ) ) & ( for u being Element of REAL 3 st u in dom F holds
F . u = H1(u) ) ) from SEQ_1:sch_3();
take  F ; ::_thesis: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,3) ) )
 for y being set st y in dom F holds
y in D by A2;
then A3: dom F c= D by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_D_holds_
y_in_dom_F
let y be set ; ::_thesis: ( y in D implies y in dom F )
assume A4: y in D ; ::_thesis: y in dom F
 D c= dom f by A1, Def3;
then  D is Subset of (REAL 3) by XBOOLE_1:1;
hence  y in dom F by A2, A4; ::_thesis: verum
end;
then  D c= dom F by TARSKI:def_3;
hence  dom F = D by A3, XBOOLE_0:def_10; ::_thesis: for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,3)
let u be Element of REAL 3; ::_thesis: ( u in D implies F . u = partdiff (f,u,3) )
assume  u in D ; ::_thesis: F . u = partdiff (f,u,3)
then  u in dom F by A2;
hence  F . u = partdiff (f,u,3) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds
b1 . u = partdiff (f,u,3) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds
b2 . u = partdiff (f,u,3) ) holds
b1 = b2
proof
let F, G be PartFunc of (REAL 3),REAL; ::_thesis: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,3) ) & dom G = D & ( for u being Element of REAL 3 st u in D holds
G . u = partdiff (f,u,3) ) implies F = G )
assume that
A5: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,3) ) ) and
A6: ( dom G = D & ( for u being Element of REAL 3 st u in D holds
G . u = partdiff (f,u,3) ) ) ; ::_thesis: F = G
now__::_thesis:_for_u_being_Element_of_REAL_3_st_u_in_dom_F_holds_
F_._u_=_G_._u
let u be Element of REAL 3; ::_thesis: ( u in dom F implies F . u = G . u )
assume A7: u in dom F ; ::_thesis: F . u = G . u
then  F . u = partdiff (f,u,3) by A5;
hence  F . u = G . u by A5, A6, A7; ::_thesis: verum
end;
hence  F = G by A5, A6, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem  defines `partial3| PDIFF_4:def_6_:_
 for f being PartFunc of (REAL 3),REAL
for D being set st f is_partial_differentiable`3_on D holds
for b3 being PartFunc of (REAL 3),REAL holds
( b3 = f `partial3| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds
b3 . u = partdiff (f,u,3) ) ) );

begin

theorem :: PDIFF_4:25
for f being PartFunc of (REAL 3),REAL
for u0 being Element of REAL 3
for N being Neighbourhood of (proj (1,3)) . u0 st f is_partial_differentiable_in u0,1 & N c= dom (SVF1 (1,f,u0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent & partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) )
proof
let f be PartFunc of (REAL 3),REAL; ::_thesis: for u0 being Element of REAL 3
for N being Neighbourhood of (proj (1,3)) . u0 st f is_partial_differentiable_in u0,1 & N c= dom (SVF1 (1,f,u0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent & partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) )
let u0 be Element of REAL 3; ::_thesis: for N being Neighbourhood of (proj (1,3)) . u0 st f is_partial_differentiable_in u0,1 & N c= dom (SVF1 (1,f,u0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent & partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) )
let N be Neighbourhood of (proj (1,3)) . u0; ::_thesis: ( f is_partial_differentiable_in u0,1 & N c= dom (SVF1 (1,f,u0)) implies for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent & partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) ) )
assume A1: ( f is_partial_differentiable_in u0,1 & N c= dom (SVF1 (1,f,u0)) ) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent & partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) )
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent & partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) )
let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent & partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) ) )
assume A2: ( rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent & partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) )
consider x0, y0, z0 being Real such that
A3: ( u0 = <*x0,y0,z0*> & ex N1 being Neighbourhood of x0 st
( N1 c= dom (SVF1 (1,f,u0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N1 holds
((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A1, Th13;
consider N1 being Neighbourhood of x0 such that
A4: ( N1 c= dom (SVF1 (1,f,u0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N1 holds
((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A3;
consider L being LinearFunc, R being RestFunc such that
A5: for x being Real st x in N1 holds
((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A4;
A6: (proj (1,3)) . u0 = x0 by A3, Th1;
then consider N2 being Neighbourhood of x0 such that
A7: ( N2 c= N & N2 c= N1 ) by RCOMP_1:17;
consider g being real number  such that
A8: ( 0 < g & N2 = ].(x0 - g),(x0 + g).[ ) by RCOMP_1:def_6;
A9: x0 in N2
proof
A10: x0 + 0 < x0 + g by A8, XREAL_1:8;
 x0 - g < x0 - 0 by A8, XREAL_1:44;
hence  x0 in N2 by A8, A10; ::_thesis: verum
end;
 ex n being Element of NAT st
( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
proof
 x0 in rng c by A2, A6, TARSKI:def_1;
then A11: lim c = x0 by SEQ_4:25;
 ( h is convergent & lim h = 0 ) ;
then A12: lim (h + c) = 0 + x0 by A11, SEQ_2:6
.= x0 ;
 h + c is convergent by SEQ_2:5;
then consider n being Element of NAT  such that
A13: for m being Element of NAT st n <= m holds
abs (((h + c) . m) - x0) < g by A8, A12, SEQ_2:def_7;
A14: rng (c ^\ n) = {x0} by A2, A6, VALUED_0:26;
take  n ; ::_thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
thus  rng (c ^\ n) c= N2 ::_thesis: rng ((h + c) ^\ n) c= N2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in N2 )
assume  y in rng (c ^\ n) ; ::_thesis: y in N2
hence  y in N2 by A9, A14, TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or y in N2 )
assume  y in rng ((h + c) ^\ n) ; ::_thesis: y in N2
then consider m being Element of NAT  such that
A15: y = ((h + c) ^\ n) . m by FUNCT_2:113;
 n + 0 <= n + m by XREAL_1:7;
then  abs (((h + c) . (n + m)) - x0) < g by A13;
then  ( - g < ((h + c) . (m + n)) - x0 & ((h + c) . (m + n)) - x0 < g ) by SEQ_2:1;
then  ( - g < (((h + c) ^\ n) . m) - x0 & (((h + c) ^\ n) . m) - x0 < g ) by NAT_1:def_3;
then  ( x0 + (- g) < ((h + c) ^\ n) . m & ((h + c) ^\ n) . m < x0 + g ) by XREAL_1:19, XREAL_1:20;
hence  y in N2 by A8, A15; ::_thesis: verum
end;
then consider n being Element of NAT  such that
A16: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 ) ;
A17: rng (c ^\ n) c= dom (SVF1 (1,f,u0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in dom (SVF1 (1,f,u0)) )
A18: rng (c ^\ n) = rng c by VALUED_0:26;
assume  y in rng (c ^\ n) ; ::_thesis: y in dom (SVF1 (1,f,u0))
then  y = x0 by A2, A6, A18, TARSKI:def_1;
then  y in N by A7, A9;
hence  y in dom (SVF1 (1,f,u0)) by A1; ::_thesis: verum
end;
A19: rng ((h + c) ^\ n) c= dom (SVF1 (1,f,u0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or y in dom (SVF1 (1,f,u0)) )
assume  y in rng ((h + c) ^\ n) ; ::_thesis: y in dom (SVF1 (1,f,u0))
then  y in N2 by A16;
then  y in N by A7;
hence  y in dom (SVF1 (1,f,u0)) by A1; ::_thesis: verum
end;
A20: rng c c= dom (SVF1 (1,f,u0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in dom (SVF1 (1,f,u0)) )
assume  y in rng c ; ::_thesis: y in dom (SVF1 (1,f,u0))
then  y = x0 by A2, A6, TARSKI:def_1;
then  y in N by A7, A9;
hence  y in dom (SVF1 (1,f,u0)) by A1; ::_thesis: verum
end;
A21: rng (h + c) c= dom (SVF1 (1,f,u0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in dom (SVF1 (1,f,u0)) )
assume  y in rng (h + c) ; ::_thesis: y in dom (SVF1 (1,f,u0))
then  y in N by A2;
hence  y in dom (SVF1 (1,f,u0)) by A1; ::_thesis: verum
end;
A22: for x being Real st x in N2 holds
((SVF1 (1,f,u0)) . x) - ((SVF1 (1,f,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5, A7;
A23: for k being Element of NAT holds ((SVF1 (1,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,u0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))
proof
let k be Element of NAT ; ::_thesis: ((SVF1 (1,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,u0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))
 ((h + c) ^\ n) . k in rng ((h + c) ^\ n) by VALUED_0:28;
then A24: ((h + c) ^\ n) . k in N2 by A16;
A25: (((h + c) ^\ n) . k) - ((c ^\ n) . k) = (((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k) by SEQM_3:15
.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by SEQ_1:7
.= (h ^\ n) . k ;
A26: (c ^\ n) . k in rng (c ^\ n) by VALUED_0:28;
 rng (c ^\ n) = rng c by VALUED_0:26;
then  (c ^\ n) . k = x0 by A2, A6, A26, TARSKI:def_1;
hence  ((SVF1 (1,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,u0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A5, A7, A24, A25; ::_thesis: verum
end;
A27: L is total by FDIFF_1:def_3;
A28: R is total by FDIFF_1:def_2;
A29: ((SVF1 (1,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,u0)) /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n))
proof
now__::_thesis:_for_k_being_Element_of_NAT_holds_(((SVF1_(1,f,u0))_/*_((h_+_c)_^\_n))_-_((SVF1_(1,f,u0))_/*_(c_^\_n)))_._k_=_((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_._k
let k be Element of NAT ; ::_thesis: (((SVF1 (1,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,u0)) /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k
thus (((SVF1 (1,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,u0)) /* (c ^\ n))) . k = (((SVF1 (1,f,u0)) /* ((h + c) ^\ n)) . k) - (((SVF1 (1,f,u0)) /* (c ^\ n)) . k) by RFUNCT_2:1
.= ((SVF1 (1,f,u0)) . (((h + c) ^\ n) . k)) - (((SVF1 (1,f,u0)) /* (c ^\ n)) . k) by A19, FUNCT_2:108
.= ((SVF1 (1,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,u0)) . ((c ^\ n) . k)) by A17, FUNCT_2:108
.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A23
.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A27, FUNCT_2:115
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A28, FUNCT_2:115
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:7 ; ::_thesis: verum
end;
hence  ((SVF1 (1,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,u0)) /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63; ::_thesis: verum
end;
A30: ( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 )
proof
deffunc H1( Element of NAT ) ->  Element of REAL = (L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . $1);
consider s1 being Real_Sequence such that
A31: for k being Element of NAT holds s1 . k = H1(k) from SEQ_1:sch_1();
consider s being Real such that
A32: for p1 being Real holds L . p1 = s * p1 by FDIFF_1:def_3;
A33: L . 1 = s * 1 by A32
.= s ;
now__::_thesis:_for_m_being_Element_of_NAT_holds_(((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_(#)_((h_^\_n)_"))_._m_=_s1_._m
let m be Element of NAT ; ::_thesis: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = s1 . m
A34: (h ^\ n) . m <> 0 by SEQ_1:5;
thus (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = (((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) ") . m) by SEQ_1:8
.= (((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) ") . m) by SEQ_1:7
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) ") . m))
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by SEQ_1:8
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by VALUED_1:10
.= ((L . ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A27, FUNCT_2:115
.= ((s * ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A32
.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)
.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A34, XCMPLX_0:def_7
.= s1 . m by A31, A33 ; ::_thesis: verum
end;
then A35: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = s1 by FUNCT_2:63;
A36: now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_n1_being_Element_of_NAT_st_
for_k_being_Element_of_NAT_st_n1_<=_k_holds_
abs_((s1_._k)_-_(L_._1))_<_r
let r be real number ; ::_thesis: ( 0 < r implies ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r )
assume A37: 0 < r ; ::_thesis: ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r
 ( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0 ) by FDIFF_1:def_2;
then consider m being Element of NAT  such that
A38: for k being Element of NAT st m <= k holds
abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) < r by A37, SEQ_2:def_7;
take n1 = m; ::_thesis: for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r
let k be Element of NAT ; ::_thesis: ( n1 <= k implies abs ((s1 . k) - (L . 1)) < r )
assume A39: n1 <= k ; ::_thesis: abs ((s1 . k) - (L . 1)) < r
abs ((s1 . k) - (L . 1)) = abs (((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L . 1)) by A31
.= abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) ;
hence  abs ((s1 . k) - (L . 1)) < r by A38, A39; ::_thesis: verum
end;
hence  ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A35, SEQ_2:def_6; ::_thesis: lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1
hence  lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 by A35, A36, SEQ_2:def_7; ::_thesis: verum
end;
A40: N2 c= dom (SVF1 (1,f,u0)) by A1, A7, XBOOLE_1:1;
A41: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = ((((SVF1 (1,f,u0)) /* (h + c)) ^\ n) - ((SVF1 (1,f,u0)) /* (c ^\ n))) (#) ((h ^\ n) ") by A21, A29, VALUED_0:27
.= ((((SVF1 (1,f,u0)) /* (h + c)) ^\ n) - (((SVF1 (1,f,u0)) /* c) ^\ n)) (#) ((h ^\ n) ") by A20, VALUED_0:27
.= ((((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) ^\ n) (#) ((h ^\ n) ") by SEQM_3:17
.= ((((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) ^\ n) (#) ((h ") ^\ n) by SEQM_3:18
.= ((((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) (#) (h ")) ^\ n by SEQM_3:19 ;
then A42: L . 1 = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) by A30, SEQ_4:22;
thus  (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent by A30, A41, SEQ_4:21; ::_thesis: partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)))
thus  partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) by A1, A3, A22, A40, A42, Th16; ::_thesis: verum
end;

theorem :: PDIFF_4:26
for f being PartFunc of (REAL 3),REAL
for u0 being Element of REAL 3
for N being Neighbourhood of (proj (2,3)) . u0 st f is_partial_differentiable_in u0,2 & N c= dom (SVF1 (2,f,u0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) is convergent & partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) )
proof
let f be PartFunc of (REAL 3),REAL; ::_thesis: for u0 being Element of REAL 3
for N being Neighbourhood of (proj (2,3)) . u0 st f is_partial_differentiable_in u0,2 & N c= dom (SVF1 (2,f,u0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) is convergent & partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) )
let u0 be Element of REAL 3; ::_thesis: for N being Neighbourhood of (proj (2,3)) . u0 st f is_partial_differentiable_in u0,2 & N c= dom (SVF1 (2,f,u0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) is convergent & partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) )
let N be Neighbourhood of (proj (2,3)) . u0; ::_thesis: ( f is_partial_differentiable_in u0,2 & N c= dom (SVF1 (2,f,u0)) implies for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) is convergent & partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) ) )
assume A1: ( f is_partial_differentiable_in u0,2 & N c= dom (SVF1 (2,f,u0)) ) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) is convergent & partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) )
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) is convergent & partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) )
let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) is convergent & partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) ) )
assume A2: ( rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) is convergent & partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) )
consider x0, y0, z0 being Real such that
A3: ( u0 = <*x0,y0,z0*> & ex N1 being Neighbourhood of y0 st
( N1 c= dom (SVF1 (2,f,u0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N1 holds
((SVF1 (2,f,u0)) . y) - ((SVF1 (2,f,u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by A1, Th14;
consider N1 being Neighbourhood of y0 such that
A4: ( N1 c= dom (SVF1 (2,f,u0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N1 holds
((SVF1 (2,f,u0)) . y) - ((SVF1 (2,f,u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A3;
consider L being LinearFunc, R being RestFunc such that
A5: for y being Real st y in N1 holds
((SVF1 (2,f,u0)) . y) - ((SVF1 (2,f,u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A4;
A6: (proj (2,3)) . u0 = y0 by A3, Th2;
then consider N2 being Neighbourhood of y0 such that
A7: ( N2 c= N & N2 c= N1 ) by RCOMP_1:17;
consider g being real number  such that
A8: ( 0 < g & N2 = ].(y0 - g),(y0 + g).[ ) by RCOMP_1:def_6;
A9: y0 in N2
proof
A10: y0 + 0 < y0 + g by A8, XREAL_1:8;
 y0 - g < y0 - 0 by A8, XREAL_1:44;
hence  y0 in N2 by A8, A10; ::_thesis: verum
end;
 ex n being Element of NAT st
( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
proof
 y0 in rng c by A2, A6, TARSKI:def_1;
then A11: lim c = y0 by SEQ_4:25;
 ( h is convergent & lim h = 0 ) ;
then A12: lim (h + c) = 0 + y0 by A11, SEQ_2:6
.= y0 ;
 h + c is convergent by SEQ_2:5;
then consider n being Element of NAT  such that
A13: for m being Element of NAT st n <= m holds
abs (((h + c) . m) - y0) < g by A8, A12, SEQ_2:def_7;
A14: rng (c ^\ n) = {y0} by A2, A6, VALUED_0:26;
take  n ; ::_thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
thus  rng (c ^\ n) c= N2 ::_thesis: rng ((h + c) ^\ n) c= N2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in N2 )
assume  y in rng (c ^\ n) ; ::_thesis: y in N2
hence  y in N2 by A9, A14, TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or y in N2 )
assume  y in rng ((h + c) ^\ n) ; ::_thesis: y in N2
then consider m being Element of NAT  such that
A15: y = ((h + c) ^\ n) . m by FUNCT_2:113;
 n + 0 <= n + m by XREAL_1:7;
then  abs (((h + c) . (n + m)) - y0) < g by A13;
then  ( - g < ((h + c) . (m + n)) - y0 & ((h + c) . (m + n)) - y0 < g ) by SEQ_2:1;
then  ( - g < (((h + c) ^\ n) . m) - y0 & (((h + c) ^\ n) . m) - y0 < g ) by NAT_1:def_3;
then  ( y0 + (- g) < ((h + c) ^\ n) . m & ((h + c) ^\ n) . m < y0 + g ) by XREAL_1:19, XREAL_1:20;
hence  y in N2 by A8, A15; ::_thesis: verum
end;
then consider n being Element of NAT  such that
A16: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 ) ;
A17: rng (c ^\ n) c= dom (SVF1 (2,f,u0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in dom (SVF1 (2,f,u0)) )
A18: rng (c ^\ n) = rng c by VALUED_0:26;
assume  y in rng (c ^\ n) ; ::_thesis: y in dom (SVF1 (2,f,u0))
then  y = y0 by A2, A6, A18, TARSKI:def_1;
then  y in N by A7, A9;
hence  y in dom (SVF1 (2,f,u0)) by A1; ::_thesis: verum
end;
A19: rng ((h + c) ^\ n) c= dom (SVF1 (2,f,u0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or y in dom (SVF1 (2,f,u0)) )
assume  y in rng ((h + c) ^\ n) ; ::_thesis: y in dom (SVF1 (2,f,u0))
then  y in N2 by A16;
then  y in N by A7;
hence  y in dom (SVF1 (2,f,u0)) by A1; ::_thesis: verum
end;
A20: rng c c= dom (SVF1 (2,f,u0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in dom (SVF1 (2,f,u0)) )
assume  y in rng c ; ::_thesis: y in dom (SVF1 (2,f,u0))
then  y = y0 by A2, A6, TARSKI:def_1;
then  y in N by A7, A9;
hence  y in dom (SVF1 (2,f,u0)) by A1; ::_thesis: verum
end;
A21: rng (h + c) c= dom (SVF1 (2,f,u0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in dom (SVF1 (2,f,u0)) )
assume  y in rng (h + c) ; ::_thesis: y in dom (SVF1 (2,f,u0))
then  y in N by A2;
hence  y in dom (SVF1 (2,f,u0)) by A1; ::_thesis: verum
end;
A22: for y being Real st y in N2 holds
((SVF1 (2,f,u0)) . y) - ((SVF1 (2,f,u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A5, A7;
A23: for k being Element of NAT holds ((SVF1 (2,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (2,f,u0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))
proof
let k be Element of NAT ; ::_thesis: ((SVF1 (2,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (2,f,u0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))
 ((h + c) ^\ n) . k in rng ((h + c) ^\ n) by VALUED_0:28;
then A24: ((h + c) ^\ n) . k in N2 by A16;
A25: (((h + c) ^\ n) . k) - ((c ^\ n) . k) = (((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k) by SEQM_3:15
.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by SEQ_1:7
.= (h ^\ n) . k ;
A26: (c ^\ n) . k in rng (c ^\ n) by VALUED_0:28;
 rng (c ^\ n) = rng c by VALUED_0:26;
then  (c ^\ n) . k = y0 by A2, A6, A26, TARSKI:def_1;
hence  ((SVF1 (2,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (2,f,u0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A5, A7, A24, A25; ::_thesis: verum
end;
A27: L is total by FDIFF_1:def_3;
A28: R is total by FDIFF_1:def_2;
A29: ((SVF1 (2,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (2,f,u0)) /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n))
proof
now__::_thesis:_for_k_being_Element_of_NAT_holds_(((SVF1_(2,f,u0))_/*_((h_+_c)_^\_n))_-_((SVF1_(2,f,u0))_/*_(c_^\_n)))_._k_=_((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_._k
let k be Element of NAT ; ::_thesis: (((SVF1 (2,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (2,f,u0)) /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k
thus (((SVF1 (2,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (2,f,u0)) /* (c ^\ n))) . k = (((SVF1 (2,f,u0)) /* ((h + c) ^\ n)) . k) - (((SVF1 (2,f,u0)) /* (c ^\ n)) . k) by RFUNCT_2:1
.= ((SVF1 (2,f,u0)) . (((h + c) ^\ n) . k)) - (((SVF1 (2,f,u0)) /* (c ^\ n)) . k) by A19, FUNCT_2:108
.= ((SVF1 (2,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (2,f,u0)) . ((c ^\ n) . k)) by A17, FUNCT_2:108
.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A23
.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A27, FUNCT_2:115
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A28, FUNCT_2:115
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:7 ; ::_thesis: verum
end;
hence  ((SVF1 (2,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (2,f,u0)) /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63; ::_thesis: verum
end;
A30: ( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 )
proof
deffunc H1( Element of NAT ) ->  Element of REAL = (L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . $1);
consider s1 being Real_Sequence such that
A31: for k being Element of NAT holds s1 . k = H1(k) from SEQ_1:sch_1();
consider s being Real such that
A32: for p1 being Real holds L . p1 = s * p1 by FDIFF_1:def_3;
A33: L . 1 = s * 1 by A32
.= s ;
now__::_thesis:_for_m_being_Element_of_NAT_holds_(((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_(#)_((h_^\_n)_"))_._m_=_s1_._m
let m be Element of NAT ; ::_thesis: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = s1 . m
A34: (h ^\ n) . m <> 0 by SEQ_1:5;
thus (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = (((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) ") . m) by SEQ_1:8
.= (((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) ") . m) by SEQ_1:7
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) ") . m))
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by SEQ_1:8
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by VALUED_1:10
.= ((L . ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A27, FUNCT_2:115
.= ((s * ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A32
.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)
.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A34, XCMPLX_0:def_7
.= s1 . m by A31, A33 ; ::_thesis: verum
end;
then A35: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = s1 by FUNCT_2:63;
A36: now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_n1_being_Element_of_NAT_st_
for_k_being_Element_of_NAT_st_n1_<=_k_holds_
abs_((s1_._k)_-_(L_._1))_<_r
let r be real number ; ::_thesis: ( 0 < r implies ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r )
assume A37: 0 < r ; ::_thesis: ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r
 ( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0 ) by FDIFF_1:def_2;
then consider m being Element of NAT  such that
A38: for k being Element of NAT st m <= k holds
abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) < r by A37, SEQ_2:def_7;
take n1 = m; ::_thesis: for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r
let k be Element of NAT ; ::_thesis: ( n1 <= k implies abs ((s1 . k) - (L . 1)) < r )
assume A39: n1 <= k ; ::_thesis: abs ((s1 . k) - (L . 1)) < r
abs ((s1 . k) - (L . 1)) = abs (((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L . 1)) by A31
.= abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) ;
hence  abs ((s1 . k) - (L . 1)) < r by A38, A39; ::_thesis: verum
end;
hence  ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A35, SEQ_2:def_6; ::_thesis: lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1
hence  lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 by A35, A36, SEQ_2:def_7; ::_thesis: verum
end;
A40: N2 c= dom (SVF1 (2,f,u0)) by A1, A7, XBOOLE_1:1;
A41: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = ((((SVF1 (2,f,u0)) /* (h + c)) ^\ n) - ((SVF1 (2,f,u0)) /* (c ^\ n))) (#) ((h ^\ n) ") by A21, A29, VALUED_0:27
.= ((((SVF1 (2,f,u0)) /* (h + c)) ^\ n) - (((SVF1 (2,f,u0)) /* c) ^\ n)) (#) ((h ^\ n) ") by A20, VALUED_0:27
.= ((((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) ^\ n) (#) ((h ^\ n) ") by SEQM_3:17
.= ((((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) ^\ n) (#) ((h ") ^\ n) by SEQM_3:18
.= ((((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) (#) (h ")) ^\ n by SEQM_3:19 ;
then A42: L . 1 = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) by A30, SEQ_4:22;
thus  (h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) is convergent by A30, A41, SEQ_4:21; ::_thesis: partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)))
thus  partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) by A1, A3, A22, A40, A42, Th17; ::_thesis: verum
end;

theorem :: PDIFF_4:27
for f being PartFunc of (REAL 3),REAL
for u0 being Element of REAL 3
for N being Neighbourhood of (proj (3,3)) . u0 st f is_partial_differentiable_in u0,3 & N c= dom (SVF1 (3,f,u0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) is convergent & partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) )
proof
let f be PartFunc of (REAL 3),REAL; ::_thesis: for u0 being Element of REAL 3
for N being Neighbourhood of (proj (3,3)) . u0 st f is_partial_differentiable_in u0,3 & N c= dom (SVF1 (3,f,u0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) is convergent & partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) )
let u0 be Element of REAL 3; ::_thesis: for N being Neighbourhood of (proj (3,3)) . u0 st f is_partial_differentiable_in u0,3 & N c= dom (SVF1 (3,f,u0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) is convergent & partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) )
let N be Neighbourhood of (proj (3,3)) . u0; ::_thesis: ( f is_partial_differentiable_in u0,3 & N c= dom (SVF1 (3,f,u0)) implies for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) is convergent & partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) ) )
assume A1: ( f is_partial_differentiable_in u0,3 & N c= dom (SVF1 (3,f,u0)) ) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) is convergent & partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) )
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) is convergent & partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) )
let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) is convergent & partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) ) )
assume A2: ( rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) is convergent & partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) )
consider x0, y0, z0 being Real such that
A3: ( u0 = <*x0,y0,z0*> & ex N1 being Neighbourhood of z0 st
( N1 c= dom (SVF1 (3,f,u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N1 holds
((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) by A1, Th15;
consider N1 being Neighbourhood of z0 such that
A4: ( N1 c= dom (SVF1 (3,f,u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N1 holds
((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) by A3;
consider L being LinearFunc, R being RestFunc such that
A5: for z being Real st z in N1 holds
((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) by A4;
A6: (proj (3,3)) . u0 = z0 by A3, Th3;
then consider N2 being Neighbourhood of z0 such that
A7: ( N2 c= N & N2 c= N1 ) by RCOMP_1:17;
consider g being real number  such that
A8: ( 0 < g & N2 = ].(z0 - g),(z0 + g).[ ) by RCOMP_1:def_6;
A9: z0 in N2
proof
A10: z0 + 0 < z0 + g by A8, XREAL_1:8;
 z0 - g < z0 - 0 by A8, XREAL_1:44;
hence  z0 in N2 by A8, A10; ::_thesis: verum
end;
 ex n being Element of NAT st
( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
proof
 z0 in rng c by A2, A6, TARSKI:def_1;
then A11: lim c = z0 by SEQ_4:25;
 ( h is convergent & lim h = 0 ) ;
then A12: lim (h + c) = 0 + z0 by A11, SEQ_2:6
.= z0 ;
 h + c is convergent by SEQ_2:5;
then consider n being Element of NAT  such that
A13: for m being Element of NAT st n <= m holds
abs (((h + c) . m) - z0) < g by A8, A12, SEQ_2:def_7;
A14: rng (c ^\ n) = {z0} by A2, A6, VALUED_0:26;
take  n ; ::_thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
thus  rng (c ^\ n) c= N2 ::_thesis: rng ((h + c) ^\ n) c= N2
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (c ^\ n) or z in N2 )
assume  z in rng (c ^\ n) ; ::_thesis: z in N2
hence  z in N2 by A9, A14, TARSKI:def_1; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng ((h + c) ^\ n) or z in N2 )
assume  z in rng ((h + c) ^\ n) ; ::_thesis: z in N2
then consider m being Element of NAT  such that
A15: z = ((h + c) ^\ n) . m by FUNCT_2:113;
 n + 0 <= n + m by XREAL_1:7;
then  abs (((h + c) . (n + m)) - z0) < g by A13;
then  ( - g < ((h + c) . (m + n)) - z0 & ((h + c) . (m + n)) - z0 < g ) by SEQ_2:1;
then  ( - g < (((h + c) ^\ n) . m) - z0 & (((h + c) ^\ n) . m) - z0 < g ) by NAT_1:def_3;
then  ( z0 + (- g) < ((h + c) ^\ n) . m & ((h + c) ^\ n) . m < z0 + g ) by XREAL_1:19, XREAL_1:20;
hence  z in N2 by A8, A15; ::_thesis: verum
end;
then consider n being Element of NAT  such that
A16: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 ) ;
A17: rng (c ^\ n) c= dom (SVF1 (3,f,u0))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (c ^\ n) or z in dom (SVF1 (3,f,u0)) )
A18: rng (c ^\ n) = rng c by VALUED_0:26;
assume  z in rng (c ^\ n) ; ::_thesis: z in dom (SVF1 (3,f,u0))
then  z = z0 by A2, A6, A18, TARSKI:def_1;
then  z in N by A7, A9;
hence  z in dom (SVF1 (3,f,u0)) by A1; ::_thesis: verum
end;
A19: rng ((h + c) ^\ n) c= dom (SVF1 (3,f,u0))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng ((h + c) ^\ n) or z in dom (SVF1 (3,f,u0)) )
assume  z in rng ((h + c) ^\ n) ; ::_thesis: z in dom (SVF1 (3,f,u0))
then  z in N2 by A16;
then  z in N by A7;
hence  z in dom (SVF1 (3,f,u0)) by A1; ::_thesis: verum
end;
A20: rng c c= dom (SVF1 (3,f,u0))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng c or z in dom (SVF1 (3,f,u0)) )
assume  z in rng c ; ::_thesis: z in dom (SVF1 (3,f,u0))
then  z = z0 by A2, A6, TARSKI:def_1;
then  z in N by A7, A9;
hence  z in dom (SVF1 (3,f,u0)) by A1; ::_thesis: verum
end;
A21: rng (h + c) c= dom (SVF1 (3,f,u0))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (h + c) or z in dom (SVF1 (3,f,u0)) )
assume  z in rng (h + c) ; ::_thesis: z in dom (SVF1 (3,f,u0))
then  z in N by A2;
hence  z in dom (SVF1 (3,f,u0)) by A1; ::_thesis: verum
end;
A22: for z being Real st z in N2 holds
((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) by A5, A7;
A23: for k being Element of NAT holds ((SVF1 (3,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (3,f,u0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))
proof
let k be Element of NAT ; ::_thesis: ((SVF1 (3,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (3,f,u0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))
 ((h + c) ^\ n) . k in rng ((h + c) ^\ n) by VALUED_0:28;
then A24: ((h + c) ^\ n) . k in N2 by A16;
A25: (((h + c) ^\ n) . k) - ((c ^\ n) . k) = (((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k) by SEQM_3:15
.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by SEQ_1:7
.= (h ^\ n) . k ;
A26: (c ^\ n) . k in rng (c ^\ n) by VALUED_0:28;
 rng (c ^\ n) = rng c by VALUED_0:26;
then  (c ^\ n) . k = z0 by A2, A6, A26, TARSKI:def_1;
hence  ((SVF1 (3,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (3,f,u0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A5, A7, A24, A25; ::_thesis: verum
end;
A27: L is total by FDIFF_1:def_3;
A28: R is total by FDIFF_1:def_2;
A29: ((SVF1 (3,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (3,f,u0)) /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n))
proof
now__::_thesis:_for_k_being_Element_of_NAT_holds_(((SVF1_(3,f,u0))_/*_((h_+_c)_^\_n))_-_((SVF1_(3,f,u0))_/*_(c_^\_n)))_._k_=_((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_._k
let k be Element of NAT ; ::_thesis: (((SVF1 (3,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (3,f,u0)) /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k
thus (((SVF1 (3,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (3,f,u0)) /* (c ^\ n))) . k = (((SVF1 (3,f,u0)) /* ((h + c) ^\ n)) . k) - (((SVF1 (3,f,u0)) /* (c ^\ n)) . k) by RFUNCT_2:1
.= ((SVF1 (3,f,u0)) . (((h + c) ^\ n) . k)) - (((SVF1 (3,f,u0)) /* (c ^\ n)) . k) by A19, FUNCT_2:108
.= ((SVF1 (3,f,u0)) . (((h + c) ^\ n) . k)) - ((SVF1 (3,f,u0)) . ((c ^\ n) . k)) by A17, FUNCT_2:108
.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A23
.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A27, FUNCT_2:115
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A28, FUNCT_2:115
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:7 ; ::_thesis: verum
end;
hence  ((SVF1 (3,f,u0)) /* ((h + c) ^\ n)) - ((SVF1 (3,f,u0)) /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63; ::_thesis: verum
end;
A30: ( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 )
proof
deffunc H1( Element of NAT ) ->  Element of REAL = (L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . $1);
consider s1 being Real_Sequence such that
A31: for k being Element of NAT holds s1 . k = H1(k) from SEQ_1:sch_1();
consider s being Real such that
A32: for p1 being Real holds L . p1 = s * p1 by FDIFF_1:def_3;
A33: L . 1 = s * 1 by A32
.= s ;
now__::_thesis:_for_m_being_Element_of_NAT_holds_(((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_(#)_((h_^\_n)_"))_._m_=_s1_._m
let m be Element of NAT ; ::_thesis: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = s1 . m
A34: (h ^\ n) . m <> 0 by SEQ_1:5;
thus (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = (((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) ") . m) by SEQ_1:8
.= (((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) ") . m) by SEQ_1:7
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) ") . m))
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by SEQ_1:8
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by VALUED_1:10
.= ((L . ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A27, FUNCT_2:115
.= ((s * ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A32
.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)
.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A34, XCMPLX_0:def_7
.= s1 . m by A31, A33 ; ::_thesis: verum
end;
then A35: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = s1 by FUNCT_2:63;
A36: now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_n1_being_Element_of_NAT_st_
for_k_being_Element_of_NAT_st_n1_<=_k_holds_
abs_((s1_._k)_-_(L_._1))_<_r
let r be real number ; ::_thesis: ( 0 < r implies ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r )
assume A37: 0 < r ; ::_thesis: ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r
 ( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0 ) by FDIFF_1:def_2;
then consider m being Element of NAT  such that
A38: for k being Element of NAT st m <= k holds
abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) < r by A37, SEQ_2:def_7;
take n1 = m; ::_thesis: for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L . 1)) < r
let k be Element of NAT ; ::_thesis: ( n1 <= k implies abs ((s1 . k) - (L . 1)) < r )
assume A39: n1 <= k ; ::_thesis: abs ((s1 . k) - (L . 1)) < r
abs ((s1 . k) - (L . 1)) = abs (((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L . 1)) by A31
.= abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) ;
hence  abs ((s1 . k) - (L . 1)) < r by A38, A39; ::_thesis: verum
end;
hence  ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A35, SEQ_2:def_6; ::_thesis: lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1
hence  lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 by A35, A36, SEQ_2:def_7; ::_thesis: verum
end;
A40: N2 c= dom (SVF1 (3,f,u0)) by A1, A7, XBOOLE_1:1;
A41: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = ((((SVF1 (3,f,u0)) /* (h + c)) ^\ n) - ((SVF1 (3,f,u0)) /* (c ^\ n))) (#) ((h ^\ n) ") by A21, A29, VALUED_0:27
.= ((((SVF1 (3,f,u0)) /* (h + c)) ^\ n) - (((SVF1 (3,f,u0)) /* c) ^\ n)) (#) ((h ^\ n) ") by A20, VALUED_0:27
.= ((((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) ^\ n) (#) ((h ^\ n) ") by SEQM_3:17
.= ((((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) ^\ n) (#) ((h ") ^\ n) by SEQM_3:18
.= ((((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) (#) (h ")) ^\ n by SEQM_3:19 ;
then A42: L . 1 = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) by A30, SEQ_4:22;
thus  (h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) is convergent by A30, A41, SEQ_4:21; ::_thesis: partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)))
thus  partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) by A1, A3, A22, A40, A42, Th18; ::_thesis: verum
end;

theorem :: PDIFF_4:28
for u0 being Element of REAL 3
for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,1 & f2 is_partial_differentiable_in u0,1 holds
f1 (#) f2 is_partial_differentiable_in u0,1
proof
let u0 be Element of REAL 3; ::_thesis: for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,1 & f2 is_partial_differentiable_in u0,1 holds
f1 (#) f2 is_partial_differentiable_in u0,1
let f1, f2 be PartFunc of (REAL 3),REAL; ::_thesis: ( f1 is_partial_differentiable_in u0,1 & f2 is_partial_differentiable_in u0,1 implies f1 (#) f2 is_partial_differentiable_in u0,1 )
assume that
A1: f1 is_partial_differentiable_in u0,1 and
A2: f2 is_partial_differentiable_in u0,1 ; ::_thesis: f1 (#) f2 is_partial_differentiable_in u0,1
consider x0, y0, z0 being Real such that
A3: ( u0 = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f1,u0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f1,u0)) . x) - ((SVF1 (1,f1,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A1, Th13;
consider N1 being Neighbourhood of x0 such that
A4: ( N1 c= dom (SVF1 (1,f1,u0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N1 holds
((SVF1 (1,f1,u0)) . x) - ((SVF1 (1,f1,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A3;
consider L1 being LinearFunc, R1 being RestFunc such that
A5: for x being Real st x in N1 holds
((SVF1 (1,f1,u0)) . x) - ((SVF1 (1,f1,u0)) . x0) = (L1 . (x - x0)) + (R1 . (x - x0)) by A4;
consider x1, y1, z1 being Real such that
A6: ( u0 = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,f2,u0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f2,u0)) . x) - ((SVF1 (1,f2,u0)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) by A2, Th13;
 ( x0 = x1 & y0 = y1 & z0 = z1 ) by A3, A6, FINSEQ_1:78;
then consider N2 being Neighbourhood of x0 such that
A7: ( N2 c= dom (SVF1 (1,f2,u0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N2 holds
((SVF1 (1,f2,u0)) . x) - ((SVF1 (1,f2,u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A6;
consider L2 being LinearFunc, R2 being RestFunc such that
A8: for x being Real st x in N2 holds
((SVF1 (1,f2,u0)) . x) - ((SVF1 (1,f2,u0)) . x0) = (L2 . (x - x0)) + (R2 . (x - x0)) by A7;
consider N being Neighbourhood of x0 such that
A9: ( N c= N1 & N c= N2 ) by RCOMP_1:17;
reconsider L11 = ((SVF1 (1,f2,u0)) . x0) (#) L1, L12 = ((SVF1 (1,f1,u0)) . x0) (#) L2 as LinearFunc by FDIFF_1:3;
A10: ( L11 is total & L12 is total & L1 is total & L2 is total ) by FDIFF_1:def_3;
reconsider L = L11 + L12 as LinearFunc by FDIFF_1:2;
reconsider R11 = ((SVF1 (1,f2,u0)) . x0) (#) R1 as RestFunc by FDIFF_1:5;
reconsider R12 = ((SVF1 (1,f1,u0)) . x0) (#) R2 as RestFunc by FDIFF_1:5;
reconsider R13 = R11 + R12 as RestFunc by FDIFF_1:4;
reconsider R14 = L1 (#) L2 as RestFunc by FDIFF_1:6;
reconsider R15 = R13 + R14 as RestFunc by FDIFF_1:4;
reconsider R16 = R1 (#) L2, R18 = R2 (#) L1 as RestFunc by FDIFF_1:7;
reconsider R17 = R1 (#) R2 as RestFunc by FDIFF_1:4;
reconsider R19 = R16 + R17 as RestFunc by FDIFF_1:4;
reconsider R20 = R19 + R18 as RestFunc by FDIFF_1:4;
reconsider R = R15 + R20 as RestFunc by FDIFF_1:4;
A11: ( R1 is total & R2 is total & R11 is total & R12 is total & R13 is total & R14 is total & R15 is total & R16 is total & R17 is total & R18 is total & R19 is total & R20 is total ) by FDIFF_1:def_2;
A12: N c= dom (SVF1 (1,f1,u0)) by A4, A9, XBOOLE_1:1;
A13: N c= dom (SVF1 (1,f2,u0)) by A7, A9, XBOOLE_1:1;
A14: for y being Real st y in N holds
y in dom (SVF1 (1,(f1 (#) f2),u0))
proof
let y be Real; ::_thesis: ( y in N implies y in dom (SVF1 (1,(f1 (#) f2),u0)) )
assume A15: y in N ; ::_thesis: y in dom (SVF1 (1,(f1 (#) f2),u0))
then A16: ( y in dom (reproj (1,u0)) & (reproj (1,u0)) . y in dom f1 ) by A12, FUNCT_1:11;
 ( y in dom (reproj (1,u0)) & (reproj (1,u0)) . y in dom f2 ) by A13, A15, FUNCT_1:11;
then  ( y in dom (reproj (1,u0)) & (reproj (1,u0)) . y in (dom f1) /\ (dom f2) ) by A16, XBOOLE_0:def_4;
then  ( y in dom (reproj (1,u0)) & (reproj (1,u0)) . y in dom (f1 (#) f2) ) by VALUED_1:def_4;
hence  y in dom (SVF1 (1,(f1 (#) f2),u0)) by FUNCT_1:11; ::_thesis: verum
end;
then  for y being set st y in N holds
y in dom (SVF1 (1,(f1 (#) f2),u0)) ;
then A17: N c= dom (SVF1 (1,(f1 (#) f2),u0)) by TARSKI:def_3;
now__::_thesis:_for_x_being_Real_st_x_in_N_holds_
((SVF1_(1,(f1_(#)_f2),u0))_._x)_-_((SVF1_(1,(f1_(#)_f2),u0))_._x0)_=_(L_._(x_-_x0))_+_(R_._(x_-_x0))
let x be Real; ::_thesis: ( x in N implies ((SVF1 (1,(f1 (#) f2),u0)) . x) - ((SVF1 (1,(f1 (#) f2),u0)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A18: x in N ; ::_thesis: ((SVF1 (1,(f1 (#) f2),u0)) . x) - ((SVF1 (1,(f1 (#) f2),u0)) . x0) = (L . (x - x0)) + (R . (x - x0))
then A19: (((SVF1 (1,f1,u0)) . x) - ((SVF1 (1,f1,u0)) . x0)) + ((SVF1 (1,f1,u0)) . x0) = ((L1 . (x - x0)) + (R1 . (x - x0))) + ((SVF1 (1,f1,u0)) . x0) by A5, A9;
 x in dom ((f1 (#) f2) * (reproj (1,u0))) by A14, A18;
then A20: ( x in dom (reproj (1,u0)) & (reproj (1,u0)) . x in dom (f1 (#) f2) ) by FUNCT_1:11;
then  (reproj (1,u0)) . x in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then  ( (reproj (1,u0)) . x in dom f1 & (reproj (1,u0)) . x in dom f2 ) by XBOOLE_0:def_4;
then A21: ( x in dom (f1 * (reproj (1,u0))) & x in dom (f2 * (reproj (1,u0))) ) by A20, FUNCT_1:11;
A22: x0 in N by RCOMP_1:16;
 x0 in dom ((f1 (#) f2) * (reproj (1,u0))) by A14, RCOMP_1:16;
then A23: ( x0 in dom (reproj (1,u0)) & (reproj (1,u0)) . x0 in dom (f1 (#) f2) ) by FUNCT_1:11;
then  (reproj (1,u0)) . x0 in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then  ( (reproj (1,u0)) . x0 in dom f1 & (reproj (1,u0)) . x0 in dom f2 ) by XBOOLE_0:def_4;
then A24: ( x0 in dom (f1 * (reproj (1,u0))) & x0 in dom (f2 * (reproj (1,u0))) ) by A23, FUNCT_1:11;
thus ((SVF1 (1,(f1 (#) f2),u0)) . x) - ((SVF1 (1,(f1 (#) f2),u0)) . x0) = ((f1 (#) f2) . ((reproj (1,u0)) . x)) - ((SVF1 (1,(f1 (#) f2),u0)) . x0) by A17, A18, FUNCT_1:12
.= ((f1 . ((reproj (1,u0)) . x)) * (f2 . ((reproj (1,u0)) . x))) - ((SVF1 (1,(f1 (#) f2),u0)) . x0) by VALUED_1:5
.= (((SVF1 (1,f1,u0)) . x) * (f2 . ((reproj (1,u0)) . x))) - ((SVF1 (1,(f1 (#) f2),u0)) . x0) by A21, FUNCT_1:12
.= (((SVF1 (1,f1,u0)) . x) * ((SVF1 (1,f2,u0)) . x)) - (((f1 (#) f2) * (reproj (1,u0))) . x0) by A21, FUNCT_1:12
.= (((SVF1 (1,f1,u0)) . x) * ((SVF1 (1,f2,u0)) . x)) - ((f1 (#) f2) . ((reproj (1,u0)) . x0)) by A17, A22, FUNCT_1:12
.= (((SVF1 (1,f1,u0)) . x) * ((SVF1 (1,f2,u0)) . x)) - ((f1 . ((reproj (1,u0)) . x0)) * (f2 . ((reproj (1,u0)) . x0))) by VALUED_1:5
.= (((SVF1 (1,f1,u0)) . x) * ((SVF1 (1,f2,u0)) . x)) - (((SVF1 (1,f1,u0)) . x0) * (f2 . ((reproj (1,u0)) . x0))) by A24, FUNCT_1:12
.= (((((SVF1 (1,f1,u0)) . x) * ((SVF1 (1,f2,u0)) . x)) + (- (((SVF1 (1,f1,u0)) . x) * ((SVF1 (1,f2,u0)) . x0)))) + (((SVF1 (1,f1,u0)) . x) * ((SVF1 (1,f2,u0)) . x0))) - (((SVF1 (1,f1,u0)) . x0) * ((SVF1 (1,f2,u0)) . x0)) by A24, FUNCT_1:12
.= (((SVF1 (1,f1,u0)) . x) * (((SVF1 (1,f2,u0)) . x) - ((SVF1 (1,f2,u0)) . x0))) + ((((SVF1 (1,f1,u0)) . x) - ((SVF1 (1,f1,u0)) . x0)) * ((SVF1 (1,f2,u0)) . x0))
.= (((SVF1 (1,f1,u0)) . x) * (((SVF1 (1,f2,u0)) . x) - ((SVF1 (1,f2,u0)) . x0))) + (((L1 . (x - x0)) + (R1 . (x - x0))) * ((SVF1 (1,f2,u0)) . x0)) by A5, A9, A18
.= (((SVF1 (1,f1,u0)) . x) * (((SVF1 (1,f2,u0)) . x) - ((SVF1 (1,f2,u0)) . x0))) + ((((SVF1 (1,f2,u0)) . x0) * (L1 . (x - x0))) + (((SVF1 (1,f2,u0)) . x0) * (R1 . (x - x0))))
.= (((SVF1 (1,f1,u0)) . x) * (((SVF1 (1,f2,u0)) . x) - ((SVF1 (1,f2,u0)) . x0))) + ((L11 . (x - x0)) + (((SVF1 (1,f2,u0)) . x0) * (R1 . (x - x0)))) by A10, RFUNCT_1:57
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) + ((SVF1 (1,f1,u0)) . x0)) * (((SVF1 (1,f2,u0)) . x) - ((SVF1 (1,f2,u0)) . x0))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A11, A19, RFUNCT_1:57
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) + ((SVF1 (1,f1,u0)) . x0)) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A8, A9, A18
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((((SVF1 (1,f1,u0)) . x0) * (L2 . (x - x0))) + (((SVF1 (1,f1,u0)) . x0) * (R2 . (x - x0))))) + ((L11 . (x - x0)) + (R11 . (x - x0)))
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + (((SVF1 (1,f1,u0)) . x0) * (R2 . (x - x0))))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A10, RFUNCT_1:57
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + (R12 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A11, RFUNCT_1:57
.= (((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + ((L11 . (x - x0)) + ((R11 . (x - x0)) + (R12 . (x - x0)))))
.= (((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + ((L11 . (x - x0)) + (R13 . (x - x0)))) by A11, RFUNCT_1:56
.= (((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + (((L11 . (x - x0)) + (L12 . (x - x0))) + (R13 . (x - x0)))
.= ((((L1 . (x - x0)) * (L2 . (x - x0))) + ((L1 . (x - x0)) * (R2 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0))) by A10, RFUNCT_1:56
.= (((R14 . (x - x0)) + ((R2 . (x - x0)) * (L1 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0))) by A10, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + (((R1 . (x - x0)) * (L2 . (x - x0))) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0))) by A10, A11, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0))) by A10, A11, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + (R17 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0))) by A11, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + (R19 . (x - x0))) + ((L . (x - x0)) + (R13 . (x - x0))) by A11, RFUNCT_1:56
.= ((R14 . (x - x0)) + ((R19 . (x - x0)) + (R18 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0)))
.= ((L . (x - x0)) + (R13 . (x - x0))) + ((R14 . (x - x0)) + (R20 . (x - x0))) by A11, RFUNCT_1:56
.= (L . (x - x0)) + (((R13 . (x - x0)) + (R14 . (x - x0))) + (R20 . (x - x0)))
.= (L . (x - x0)) + ((R15 . (x - x0)) + (R20 . (x - x0))) by A11, RFUNCT_1:56
.= (L . (x - x0)) + (R . (x - x0)) by A11, RFUNCT_1:56 ; ::_thesis: verum
end;
hence  f1 (#) f2 is_partial_differentiable_in u0,1 by A3, A17, Th13; ::_thesis: verum
end;

theorem :: PDIFF_4:29
for u0 being Element of REAL 3
for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,2 & f2 is_partial_differentiable_in u0,2 holds
f1 (#) f2 is_partial_differentiable_in u0,2
proof
let u0 be Element of REAL 3; ::_thesis: for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,2 & f2 is_partial_differentiable_in u0,2 holds
f1 (#) f2 is_partial_differentiable_in u0,2
let f1, f2 be PartFunc of (REAL 3),REAL; ::_thesis: ( f1 is_partial_differentiable_in u0,2 & f2 is_partial_differentiable_in u0,2 implies f1 (#) f2 is_partial_differentiable_in u0,2 )
assume that
A1: f1 is_partial_differentiable_in u0,2 and
A2: f2 is_partial_differentiable_in u0,2 ; ::_thesis: f1 (#) f2 is_partial_differentiable_in u0,2
consider x0, y0, z0 being Real such that
A3: ( u0 = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f1,u0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f1,u0)) . y) - ((SVF1 (2,f1,u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by A1, Th14;
consider N1 being Neighbourhood of y0 such that
A4: ( N1 c= dom (SVF1 (2,f1,u0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N1 holds
((SVF1 (2,f1,u0)) . y) - ((SVF1 (2,f1,u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A3;
consider L1 being LinearFunc, R1 being RestFunc such that
A5: for y being Real st y in N1 holds
((SVF1 (2,f1,u0)) . y) - ((SVF1 (2,f1,u0)) . y0) = (L1 . (y - y0)) + (R1 . (y - y0)) by A4;
consider x1, y1, z1 being Real such that
A6: ( u0 = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,f2,u0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f2,u0)) . y) - ((SVF1 (2,f2,u0)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) by A2, Th14;
 ( x0 = x1 & y0 = y1 & z0 = z1 ) by A3, A6, FINSEQ_1:78;
then consider N2 being Neighbourhood of y0 such that
A7: ( N2 c= dom (SVF1 (2,f2,u0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N2 holds
((SVF1 (2,f2,u0)) . y) - ((SVF1 (2,f2,u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A6;
consider L2 being LinearFunc, R2 being RestFunc such that
A8: for y being Real st y in N2 holds
((SVF1 (2,f2,u0)) . y) - ((SVF1 (2,f2,u0)) . y0) = (L2 . (y - y0)) + (R2 . (y - y0)) by A7;
consider N being Neighbourhood of y0 such that
A9: ( N c= N1 & N c= N2 ) by RCOMP_1:17;
reconsider L11 = ((SVF1 (2,f2,u0)) . y0) (#) L1 as LinearFunc by FDIFF_1:3;
reconsider L12 = ((SVF1 (2,f1,u0)) . y0) (#) L2 as LinearFunc by FDIFF_1:3;
A10: ( L11 is total & L12 is total & L1 is total & L2 is total ) by FDIFF_1:def_3;
reconsider L = L11 + L12 as LinearFunc by FDIFF_1:2;
reconsider R11 = ((SVF1 (2,f2,u0)) . y0) (#) R1, R12 = ((SVF1 (2,f1,u0)) . y0) (#) R2 as RestFunc by FDIFF_1:5;
reconsider R13 = R11 + R12 as RestFunc by FDIFF_1:4;
reconsider R14 = L1 (#) L2 as RestFunc by FDIFF_1:6;
reconsider R15 = R13 + R14, R17 = R1 (#) R2 as RestFunc by FDIFF_1:4;
reconsider R16 = R1 (#) L2, R18 = R2 (#) L1 as RestFunc by FDIFF_1:7;
reconsider R19 = R16 + R17 as RestFunc by FDIFF_1:4;
reconsider R20 = R19 + R18 as RestFunc by FDIFF_1:4;
reconsider R = R15 + R20 as RestFunc by FDIFF_1:4;
A11: ( R1 is total & R2 is total & R11 is total & R12 is total & R13 is total & R14 is total & R15 is total & R16 is total & R17 is total & R18 is total & R19 is total & R20 is total ) by FDIFF_1:def_2;
A12: N c= dom (SVF1 (2,f1,u0)) by A4, A9, XBOOLE_1:1;
A13: N c= dom (SVF1 (2,f2,u0)) by A7, A9, XBOOLE_1:1;
A14: for y being Real st y in N holds
y in dom (SVF1 (2,(f1 (#) f2),u0))
proof
let y be Real; ::_thesis: ( y in N implies y in dom (SVF1 (2,(f1 (#) f2),u0)) )
assume A15: y in N ; ::_thesis: y in dom (SVF1 (2,(f1 (#) f2),u0))
then A16: ( y in dom (reproj (2,u0)) & (reproj (2,u0)) . y in dom f1 ) by A12, FUNCT_1:11;
 ( y in dom (reproj (2,u0)) & (reproj (2,u0)) . y in dom f2 ) by A13, A15, FUNCT_1:11;
then  ( y in dom (reproj (2,u0)) & (reproj (2,u0)) . y in (dom f1) /\ (dom f2) ) by A16, XBOOLE_0:def_4;
then  ( y in dom (reproj (2,u0)) & (reproj (2,u0)) . y in dom (f1 (#) f2) ) by VALUED_1:def_4;
hence  y in dom (SVF1 (2,(f1 (#) f2),u0)) by FUNCT_1:11; ::_thesis: verum
end;
then  for y being set st y in N holds
y in dom (SVF1 (2,(f1 (#) f2),u0)) ;
then A17: N c= dom (SVF1 (2,(f1 (#) f2),u0)) by TARSKI:def_3;
now__::_thesis:_for_y_being_Real_st_y_in_N_holds_
((SVF1_(2,(f1_(#)_f2),u0))_._y)_-_((SVF1_(2,(f1_(#)_f2),u0))_._y0)_=_(L_._(y_-_y0))_+_(R_._(y_-_y0))
let y be Real; ::_thesis: ( y in N implies ((SVF1 (2,(f1 (#) f2),u0)) . y) - ((SVF1 (2,(f1 (#) f2),u0)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
assume A18: y in N ; ::_thesis: ((SVF1 (2,(f1 (#) f2),u0)) . y) - ((SVF1 (2,(f1 (#) f2),u0)) . y0) = (L . (y - y0)) + (R . (y - y0))
then A19: (((SVF1 (2,f1,u0)) . y) - ((SVF1 (2,f1,u0)) . y0)) + ((SVF1 (2,f1,u0)) . y0) = ((L1 . (y - y0)) + (R1 . (y - y0))) + ((SVF1 (2,f1,u0)) . y0) by A5, A9;
 y in dom ((f1 (#) f2) * (reproj (2,u0))) by A14, A18;
then A20: ( y in dom (reproj (2,u0)) & (reproj (2,u0)) . y in dom (f1 (#) f2) ) by FUNCT_1:11;
then  (reproj (2,u0)) . y in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then  ( (reproj (2,u0)) . y in dom f1 & (reproj (2,u0)) . y in dom f2 ) by XBOOLE_0:def_4;
then A21: ( y in dom (f1 * (reproj (2,u0))) & y in dom (f2 * (reproj (2,u0))) ) by A20, FUNCT_1:11;
A22: y0 in N by RCOMP_1:16;
 y0 in dom ((f1 (#) f2) * (reproj (2,u0))) by A14, RCOMP_1:16;
then A23: ( y0 in dom (reproj (2,u0)) & (reproj (2,u0)) . y0 in dom (f1 (#) f2) ) by FUNCT_1:11;
then  (reproj (2,u0)) . y0 in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then  ( (reproj (2,u0)) . y0 in dom f1 & (reproj (2,u0)) . y0 in dom f2 ) by XBOOLE_0:def_4;
then A24: ( y0 in dom (f1 * (reproj (2,u0))) & y0 in dom (f2 * (reproj (2,u0))) ) by A23, FUNCT_1:11;
thus ((SVF1 (2,(f1 (#) f2),u0)) . y) - ((SVF1 (2,(f1 (#) f2),u0)) . y0) = ((f1 (#) f2) . ((reproj (2,u0)) . y)) - ((SVF1 (2,(f1 (#) f2),u0)) . y0) by A17, A18, FUNCT_1:12
.= ((f1 . ((reproj (2,u0)) . y)) * (f2 . ((reproj (2,u0)) . y))) - ((SVF1 (2,(f1 (#) f2),u0)) . y0) by VALUED_1:5
.= (((SVF1 (2,f1,u0)) . y) * (f2 . ((reproj (2,u0)) . y))) - ((SVF1 (2,(f1 (#) f2),u0)) . y0) by A21, FUNCT_1:12
.= (((SVF1 (2,f1,u0)) . y) * ((SVF1 (2,f2,u0)) . y)) - (((f1 (#) f2) * (reproj (2,u0))) . y0) by A21, FUNCT_1:12
.= (((SVF1 (2,f1,u0)) . y) * ((SVF1 (2,f2,u0)) . y)) - ((f1 (#) f2) . ((reproj (2,u0)) . y0)) by A17, A22, FUNCT_1:12
.= (((SVF1 (2,f1,u0)) . y) * ((SVF1 (2,f2,u0)) . y)) - ((f1 . ((reproj (2,u0)) . y0)) * (f2 . ((reproj (2,u0)) . y0))) by VALUED_1:5
.= (((SVF1 (2,f1,u0)) . y) * ((SVF1 (2,f2,u0)) . y)) - (((SVF1 (2,f1,u0)) . y0) * (f2 . ((reproj (2,u0)) . y0))) by A24, FUNCT_1:12
.= (((((SVF1 (2,f1,u0)) . y) * ((SVF1 (2,f2,u0)) . y)) + (- (((SVF1 (2,f1,u0)) . y) * ((SVF1 (2,f2,u0)) . y0)))) + (((SVF1 (2,f1,u0)) . y) * ((SVF1 (2,f2,u0)) . y0))) - (((SVF1 (2,f1,u0)) . y0) * ((SVF1 (2,f2,u0)) . y0)) by A24, FUNCT_1:12
.= (((SVF1 (2,f1,u0)) . y) * (((SVF1 (2,f2,u0)) . y) - ((SVF1 (2,f2,u0)) . y0))) + ((((SVF1 (2,f1,u0)) . y) - ((SVF1 (2,f1,u0)) . y0)) * ((SVF1 (2,f2,u0)) . y0))
.= (((SVF1 (2,f1,u0)) . y) * (((SVF1 (2,f2,u0)) . y) - ((SVF1 (2,f2,u0)) . y0))) + (((L1 . (y - y0)) + (R1 . (y - y0))) * ((SVF1 (2,f2,u0)) . y0)) by A5, A9, A18
.= (((SVF1 (2,f1,u0)) . y) * (((SVF1 (2,f2,u0)) . y) - ((SVF1 (2,f2,u0)) . y0))) + ((((SVF1 (2,f2,u0)) . y0) * (L1 . (y - y0))) + (((SVF1 (2,f2,u0)) . y0) * (R1 . (y - y0))))
.= (((SVF1 (2,f1,u0)) . y) * (((SVF1 (2,f2,u0)) . y) - ((SVF1 (2,f2,u0)) . y0))) + ((L11 . (y - y0)) + (((SVF1 (2,f2,u0)) . y0) * (R1 . (y - y0)))) by A10, RFUNCT_1:57
.= ((((L1 . (y - y0)) + (R1 . (y - y0))) + ((SVF1 (2,f1,u0)) . y0)) * (((SVF1 (2,f2,u0)) . y) - ((SVF1 (2,f2,u0)) . y0))) + ((L11 . (y - y0)) + (R11 . (y - y0))) by A11, A19, RFUNCT_1:57
.= ((((L1 . (y - y0)) + (R1 . (y - y0))) + ((SVF1 (2,f1,u0)) . y0)) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L11 . (y - y0)) + (R11 . (y - y0))) by A8, A9, A18
.= ((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((((SVF1 (2,f1,u0)) . y0) * (L2 . (y - y0))) + (((SVF1 (2,f1,u0)) . y0) * (R2 . (y - y0))))) + ((L11 . (y - y0)) + (R11 . (y - y0)))
.= ((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + (((SVF1 (2,f1,u0)) . y0) * (R2 . (y - y0))))) + ((L11 . (y - y0)) + (R11 . (y - y0))) by A10, RFUNCT_1:57
.= ((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + (R12 . (y - y0)))) + ((L11 . (y - y0)) + (R11 . (y - y0))) by A11, RFUNCT_1:57
.= (((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + ((L11 . (y - y0)) + ((R11 . (y - y0)) + (R12 . (y - y0)))))
.= (((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + ((L11 . (y - y0)) + (R13 . (y - y0)))) by A11, RFUNCT_1:56
.= (((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + (((L11 . (y - y0)) + (L12 . (y - y0))) + (R13 . (y - y0)))
.= ((((L1 . (y - y0)) * (L2 . (y - y0))) + ((L1 . (y - y0)) * (R2 . (y - y0)))) + ((R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0))))) + ((L . (y - y0)) + (R13 . (y - y0))) by A10, RFUNCT_1:56
.= (((R14 . (y - y0)) + ((R2 . (y - y0)) * (L1 . (y - y0)))) + ((R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0))))) + ((L . (y - y0)) + (R13 . (y - y0))) by A10, RFUNCT_1:56
.= (((R14 . (y - y0)) + (R18 . (y - y0))) + (((R1 . (y - y0)) * (L2 . (y - y0))) + ((R1 . (y - y0)) * (R2 . (y - y0))))) + ((L . (y - y0)) + (R13 . (y - y0))) by A10, A11, RFUNCT_1:56
.= (((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + ((R1 . (y - y0)) * (R2 . (y - y0))))) + ((L . (y - y0)) + (R13 . (y - y0))) by A10, A11, RFUNCT_1:56
.= (((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + (R17 . (y - y0)))) + ((L . (y - y0)) + (R13 . (y - y0))) by A11, RFUNCT_1:56
.= (((R14 . (y - y0)) + (R18 . (y - y0))) + (R19 . (y - y0))) + ((L . (y - y0)) + (R13 . (y - y0))) by A11, RFUNCT_1:56
.= ((R14 . (y - y0)) + ((R19 . (y - y0)) + (R18 . (y - y0)))) + ((L . (y - y0)) + (R13 . (y - y0)))
.= ((L . (y - y0)) + (R13 . (y - y0))) + ((R14 . (y - y0)) + (R20 . (y - y0))) by A11, RFUNCT_1:56
.= (L . (y - y0)) + (((R13 . (y - y0)) + (R14 . (y - y0))) + (R20 . (y - y0)))
.= (L . (y - y0)) + ((R15 . (y - y0)) + (R20 . (y - y0))) by A11, RFUNCT_1:56
.= (L . (y - y0)) + (R . (y - y0)) by A11, RFUNCT_1:56 ; ::_thesis: verum
end;
hence  f1 (#) f2 is_partial_differentiable_in u0,2 by A3, A17, Th14; ::_thesis: verum
end;

theorem :: PDIFF_4:30
for u0 being Element of REAL 3
for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,3 & f2 is_partial_differentiable_in u0,3 holds
f1 (#) f2 is_partial_differentiable_in u0,3
proof
let u0 be Element of REAL 3; ::_thesis: for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,3 & f2 is_partial_differentiable_in u0,3 holds
f1 (#) f2 is_partial_differentiable_in u0,3
let f1, f2 be PartFunc of (REAL 3),REAL; ::_thesis: ( f1 is_partial_differentiable_in u0,3 & f2 is_partial_differentiable_in u0,3 implies f1 (#) f2 is_partial_differentiable_in u0,3 )
assume that
A1: f1 is_partial_differentiable_in u0,3 and
A2: f2 is_partial_differentiable_in u0,3 ; ::_thesis: f1 (#) f2 is_partial_differentiable_in u0,3
consider x0, y0, z0 being Real such that
A3: ( u0 = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,f1,u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f1,u0)) . z) - ((SVF1 (3,f1,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) by A1, Th15;
consider N1 being Neighbourhood of z0 such that
A4: ( N1 c= dom (SVF1 (3,f1,u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N1 holds
((SVF1 (3,f1,u0)) . z) - ((SVF1 (3,f1,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) by A3;
consider L1 being LinearFunc, R1 being RestFunc such that
A5: for z being Real st z in N1 holds
((SVF1 (3,f1,u0)) . z) - ((SVF1 (3,f1,u0)) . z0) = (L1 . (z - z0)) + (R1 . (z - z0)) by A4;
consider x1, y1, z1 being Real such that
A6: ( u0 = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
( N c= dom (SVF1 (3,f2,u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z1) = (L . (z - z1)) + (R . (z - z1)) ) ) by A2, Th15;
 ( x0 = x1 & y0 = y1 & z0 = z1 ) by A3, A6, FINSEQ_1:78;
then consider N2 being Neighbourhood of z0 such that
A7: ( N2 c= dom (SVF1 (3,f2,u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N2 holds
((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) by A6;
consider L2 being LinearFunc, R2 being RestFunc such that
A8: for z being Real st z in N2 holds
((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0) = (L2 . (z - z0)) + (R2 . (z - z0)) by A7;
consider N being Neighbourhood of z0 such that
A9: ( N c= N1 & N c= N2 ) by RCOMP_1:17;
reconsider L11 = ((SVF1 (3,f2,u0)) . z0) (#) L1 as LinearFunc by FDIFF_1:3;
reconsider L12 = ((SVF1 (3,f1,u0)) . z0) (#) L2 as LinearFunc by FDIFF_1:3;
A10: ( L11 is total & L12 is total & L1 is total & L2 is total ) by FDIFF_1:def_3;
reconsider L = L11 + L12 as LinearFunc by FDIFF_1:2;
reconsider R11 = ((SVF1 (3,f2,u0)) . z0) (#) R1, R12 = ((SVF1 (3,f1,u0)) . z0) (#) R2 as RestFunc by FDIFF_1:5;
reconsider R13 = R11 + R12 as RestFunc by FDIFF_1:4;
reconsider R14 = L1 (#) L2 as RestFunc by FDIFF_1:6;
reconsider R15 = R13 + R14, R17 = R1 (#) R2 as RestFunc by FDIFF_1:4;
reconsider R16 = R1 (#) L2, R18 = R2 (#) L1 as RestFunc by FDIFF_1:7;
reconsider R19 = R16 + R17 as RestFunc by FDIFF_1:4;
reconsider R20 = R19 + R18 as RestFunc by FDIFF_1:4;
reconsider R = R15 + R20 as RestFunc by FDIFF_1:4;
A11: ( R1 is total & R2 is total & R11 is total & R12 is total & R13 is total & R14 is total & R15 is total & R16 is total & R17 is total & R18 is total & R19 is total & R20 is total ) by FDIFF_1:def_2;
A12: N c= dom (SVF1 (3,f1,u0)) by A4, A9, XBOOLE_1:1;
A13: N c= dom (SVF1 (3,f2,u0)) by A7, A9, XBOOLE_1:1;
A14: for z being Real st z in N holds
z in dom (SVF1 (3,(f1 (#) f2),u0))
proof
let z be Real; ::_thesis: ( z in N implies z in dom (SVF1 (3,(f1 (#) f2),u0)) )
assume A15: z in N ; ::_thesis: z in dom (SVF1 (3,(f1 (#) f2),u0))
then A16: ( z in dom (reproj (3,u0)) & (reproj (3,u0)) . z in dom f1 ) by A12, FUNCT_1:11;
 ( z in dom (reproj (3,u0)) & (reproj (3,u0)) . z in dom f2 ) by A13, A15, FUNCT_1:11;
then  ( z in dom (reproj (3,u0)) & (reproj (3,u0)) . z in (dom f1) /\ (dom f2) ) by A16, XBOOLE_0:def_4;
then  ( z in dom (reproj (3,u0)) & (reproj (3,u0)) . z in dom (f1 (#) f2) ) by VALUED_1:def_4;
hence  z in dom (SVF1 (3,(f1 (#) f2),u0)) by FUNCT_1:11; ::_thesis: verum
end;
then  for z being set st z in N holds
z in dom (SVF1 (3,(f1 (#) f2),u0)) ;
then A17: N c= dom (SVF1 (3,(f1 (#) f2),u0)) by TARSKI:def_3;
now__::_thesis:_for_z_being_Real_st_z_in_N_holds_
((SVF1_(3,(f1_(#)_f2),u0))_._z)_-_((SVF1_(3,(f1_(#)_f2),u0))_._z0)_=_(L_._(z_-_z0))_+_(R_._(z_-_z0))
let z be Real; ::_thesis: ( z in N implies ((SVF1 (3,(f1 (#) f2),u0)) . z) - ((SVF1 (3,(f1 (#) f2),u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) )
assume A18: z in N ; ::_thesis: ((SVF1 (3,(f1 (#) f2),u0)) . z) - ((SVF1 (3,(f1 (#) f2),u0)) . z0) = (L . (z - z0)) + (R . (z - z0))
then A19: (((SVF1 (3,f1,u0)) . z) - ((SVF1 (3,f1,u0)) . z0)) + ((SVF1 (3,f1,u0)) . z0) = ((L1 . (z - z0)) + (R1 . (z - z0))) + ((SVF1 (3,f1,u0)) . z0) by A5, A9;
 z in dom ((f1 (#) f2) * (reproj (3,u0))) by A14, A18;
then A20: ( z in dom (reproj (3,u0)) & (reproj (3,u0)) . z in dom (f1 (#) f2) ) by FUNCT_1:11;
then  (reproj (3,u0)) . z in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then  ( (reproj (3,u0)) . z in dom f1 & (reproj (3,u0)) . z in dom f2 ) by XBOOLE_0:def_4;
then A21: ( z in dom (f1 * (reproj (3,u0))) & z in dom (f2 * (reproj (3,u0))) ) by A20, FUNCT_1:11;
A22: z0 in N by RCOMP_1:16;
 z0 in dom ((f1 (#) f2) * (reproj (3,u0))) by A14, RCOMP_1:16;
then A23: ( z0 in dom (reproj (3,u0)) & (reproj (3,u0)) . z0 in dom (f1 (#) f2) ) by FUNCT_1:11;
then  (reproj (3,u0)) . z0 in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then  ( (reproj (3,u0)) . z0 in dom f1 & (reproj (3,u0)) . z0 in dom f2 ) by XBOOLE_0:def_4;
then A24: ( z0 in dom (f1 * (reproj (3,u0))) & z0 in dom (f2 * (reproj (3,u0))) ) by A23, FUNCT_1:11;
thus ((SVF1 (3,(f1 (#) f2),u0)) . z) - ((SVF1 (3,(f1 (#) f2),u0)) . z0) = ((f1 (#) f2) . ((reproj (3,u0)) . z)) - ((SVF1 (3,(f1 (#) f2),u0)) . z0) by A17, A18, FUNCT_1:12
.= ((f1 . ((reproj (3,u0)) . z)) * (f2 . ((reproj (3,u0)) . z))) - ((SVF1 (3,(f1 (#) f2),u0)) . z0) by VALUED_1:5
.= (((SVF1 (3,f1,u0)) . z) * (f2 . ((reproj (3,u0)) . z))) - ((SVF1 (3,(f1 (#) f2),u0)) . z0) by A21, FUNCT_1:12
.= (((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z)) - (((f1 (#) f2) * (reproj (3,u0))) . z0) by A21, FUNCT_1:12
.= (((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z)) - ((f1 (#) f2) . ((reproj (3,u0)) . z0)) by A17, A22, FUNCT_1:12
.= (((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z)) - ((f1 . ((reproj (3,u0)) . z0)) * (f2 . ((reproj (3,u0)) . z0))) by VALUED_1:5
.= (((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z)) - (((SVF1 (3,f1,u0)) . z0) * (f2 . ((reproj (3,u0)) . z0))) by A24, FUNCT_1:12
.= (((((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z)) + (- (((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z0)))) + (((SVF1 (3,f1,u0)) . z) * ((SVF1 (3,f2,u0)) . z0))) - (((SVF1 (3,f1,u0)) . z0) * ((SVF1 (3,f2,u0)) . z0)) by A24, FUNCT_1:12
.= (((SVF1 (3,f1,u0)) . z) * (((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0))) + ((((SVF1 (3,f1,u0)) . z) - ((SVF1 (3,f1,u0)) . z0)) * ((SVF1 (3,f2,u0)) . z0))
.= (((SVF1 (3,f1,u0)) . z) * (((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0))) + (((L1 . (z - z0)) + (R1 . (z - z0))) * ((SVF1 (3,f2,u0)) . z0)) by A5, A9, A18
.= (((SVF1 (3,f1,u0)) . z) * (((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0))) + ((((SVF1 (3,f2,u0)) . z0) * (L1 . (z - z0))) + (((SVF1 (3,f2,u0)) . z0) * (R1 . (z - z0))))
.= (((SVF1 (3,f1,u0)) . z) * (((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0))) + ((L11 . (z - z0)) + (((SVF1 (3,f2,u0)) . z0) * (R1 . (z - z0)))) by A10, RFUNCT_1:57
.= ((((L1 . (z - z0)) + (R1 . (z - z0))) + ((SVF1 (3,f1,u0)) . z0)) * (((SVF1 (3,f2,u0)) . z) - ((SVF1 (3,f2,u0)) . z0))) + ((L11 . (z - z0)) + (R11 . (z - z0))) by A11, A19, RFUNCT_1:57
.= ((((L1 . (z - z0)) + (R1 . (z - z0))) + ((SVF1 (3,f1,u0)) . z0)) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + ((L11 . (z - z0)) + (R11 . (z - z0))) by A8, A9, A18
.= ((((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + ((((SVF1 (3,f1,u0)) . z0) * (L2 . (z - z0))) + (((SVF1 (3,f1,u0)) . z0) * (R2 . (z - z0))))) + ((L11 . (z - z0)) + (R11 . (z - z0)))
.= ((((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + ((L12 . (z - z0)) + (((SVF1 (3,f1,u0)) . z0) * (R2 . (z - z0))))) + ((L11 . (z - z0)) + (R11 . (z - z0))) by A10, RFUNCT_1:57
.= ((((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + ((L12 . (z - z0)) + (R12 . (z - z0)))) + ((L11 . (z - z0)) + (R11 . (z - z0))) by A11, RFUNCT_1:57
.= (((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + ((L12 . (z - z0)) + ((L11 . (z - z0)) + ((R11 . (z - z0)) + (R12 . (z - z0)))))
.= (((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + ((L12 . (z - z0)) + ((L11 . (z - z0)) + (R13 . (z - z0)))) by A11, RFUNCT_1:56
.= (((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + (((L11 . (z - z0)) + (L12 . (z - z0))) + (R13 . (z - z0)))
.= ((((L1 . (z - z0)) * (L2 . (z - z0))) + ((L1 . (z - z0)) * (R2 . (z - z0)))) + ((R1 . (z - z0)) * ((L2 . (z - z0)) + (R2 . (z - z0))))) + ((L . (z - z0)) + (R13 . (z - z0))) by A10, RFUNCT_1:56
.= (((R14 . (z - z0)) + ((R2 . (z - z0)) * (L1 . (z - z0)))) + ((R1 . (z - z0)) * ((L2 . (z - z0)) + (R2 . (z - z0))))) + ((L . (z - z0)) + (R13 . (z - z0))) by A10, RFUNCT_1:56
.= (((R14 . (z - z0)) + (R18 . (z - z0))) + (((R1 . (z - z0)) * (L2 . (z - z0))) + ((R1 . (z - z0)) * (R2 . (z - z0))))) + ((L . (z - z0)) + (R13 . (z - z0))) by A10, A11, RFUNCT_1:56
.= (((R14 . (z - z0)) + (R18 . (z - z0))) + ((R16 . (z - z0)) + ((R1 . (z - z0)) * (R2 . (z - z0))))) + ((L . (z - z0)) + (R13 . (z - z0))) by A10, A11, RFUNCT_1:56
.= (((R14 . (z - z0)) + (R18 . (z - z0))) + ((R16 . (z - z0)) + (R17 . (z - z0)))) + ((L . (z - z0)) + (R13 . (z - z0))) by A11, RFUNCT_1:56
.= (((R14 . (z - z0)) + (R18 . (z - z0))) + (R19 . (z - z0))) + ((L . (z - z0)) + (R13 . (z - z0))) by A11, RFUNCT_1:56
.= ((R14 . (z - z0)) + ((R19 . (z - z0)) + (R18 . (z - z0)))) + ((L . (z - z0)) + (R13 . (z - z0)))
.= ((L . (z - z0)) + (R13 . (z - z0))) + ((R14 . (z - z0)) + (R20 . (z - z0))) by A11, RFUNCT_1:56
.= (L . (z - z0)) + (((R13 . (z - z0)) + (R14 . (z - z0))) + (R20 . (z - z0)))
.= (L . (z - z0)) + ((R15 . (z - z0)) + (R20 . (z - z0))) by A11, RFUNCT_1:56
.= (L . (z - z0)) + (R . (z - z0)) by A11, RFUNCT_1:56 ; ::_thesis: verum
end;
hence  f1 (#) f2 is_partial_differentiable_in u0,3 by A3, A17, Th15; ::_thesis: verum
end;

theorem :: PDIFF_4:31
for f being PartFunc of (REAL 3),REAL
for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,1 holds
SVF1 (1,f,u0) is_continuous_in (proj (1,3)) . u0
proof
let f be PartFunc of (REAL 3),REAL; ::_thesis: for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,1 holds
SVF1 (1,f,u0) is_continuous_in (proj (1,3)) . u0
let u0 be Element of REAL 3; ::_thesis: ( f is_partial_differentiable_in u0,1 implies SVF1 (1,f,u0) is_continuous_in (proj (1,3)) . u0 )
assume  f is_partial_differentiable_in u0,1 ; ::_thesis: SVF1 (1,f,u0) is_continuous_in (proj (1,3)) . u0
then consider x0, y0, z0 being Real such that
A1: ( u0 = <*x0,y0,z0*> & SVF1 (1,f,u0) is_differentiable_in x0 ) by Th7;
 SVF1 (1,f,u0) is_continuous_in x0 by A1, FDIFF_1:24;
hence  SVF1 (1,f,u0) is_continuous_in (proj (1,3)) . u0 by A1, Th1; ::_thesis: verum
end;

theorem :: PDIFF_4:32
for f being PartFunc of (REAL 3),REAL
for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,2 holds
SVF1 (2,f,u0) is_continuous_in (proj (2,3)) . u0
proof
let f be PartFunc of (REAL 3),REAL; ::_thesis: for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,2 holds
SVF1 (2,f,u0) is_continuous_in (proj (2,3)) . u0
let u0 be Element of REAL 3; ::_thesis: ( f is_partial_differentiable_in u0,2 implies SVF1 (2,f,u0) is_continuous_in (proj (2,3)) . u0 )
assume  f is_partial_differentiable_in u0,2 ; ::_thesis: SVF1 (2,f,u0) is_continuous_in (proj (2,3)) . u0
then consider x0, y0, z0 being Real such that
A1: ( u0 = <*x0,y0,z0*> & SVF1 (2,f,u0) is_differentiable_in y0 ) by Th8;
 SVF1 (2,f,u0) is_continuous_in y0 by A1, FDIFF_1:24;
hence  SVF1 (2,f,u0) is_continuous_in (proj (2,3)) . u0 by A1, Th2; ::_thesis: verum
end;

theorem :: PDIFF_4:33
for f being PartFunc of (REAL 3),REAL
for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,3 holds
SVF1 (3,f,u0) is_continuous_in (proj (3,3)) . u0
proof
let f be PartFunc of (REAL 3),REAL; ::_thesis: for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,3 holds
SVF1 (3,f,u0) is_continuous_in (proj (3,3)) . u0
let u0 be Element of REAL 3; ::_thesis: ( f is_partial_differentiable_in u0,3 implies SVF1 (3,f,u0) is_continuous_in (proj (3,3)) . u0 )
assume  f is_partial_differentiable_in u0,3 ; ::_thesis: SVF1 (3,f,u0) is_continuous_in (proj (3,3)) . u0
then consider x0, y0, z0 being Real such that
A1: ( u0 = <*x0,y0,z0*> & SVF1 (3,f,u0) is_differentiable_in z0 ) by Th9;
 SVF1 (3,f,u0) is_continuous_in z0 by A1, FDIFF_1:24;
hence  SVF1 (3,f,u0) is_continuous_in (proj (3,3)) . u0 by A1, Th3; ::_thesis: verum
end;

begin

Lm4:  for x1, y1, z1, x2, y2, z2 being Real holds |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|
proof
let x1, y1, z1, x2, y2, z2 be Real; ::_thesis: |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|
A1: |[x2,y2,z2]| . 1 = x2 by FINSEQ_1:45;
A2: |[x2,y2,z2]| . 2 = y2 by FINSEQ_1:45;
A3: |[x2,y2,z2]| . 3 = z2 by FINSEQ_1:45;
A4: (|[x1,y1,z1]| . 1) + (|[x2,y2,z2]| . 1) = x1 + x2 by A1, FINSEQ_1:45;
A5: (|[x1,y1,z1]| . 2) + (|[x2,y2,z2]| . 2) = y1 + y2 by A2, FINSEQ_1:45;
 (|[x1,y1,z1]| . 3) + (|[x2,y2,z2]| . 3) = z1 + z2 by A3, FINSEQ_1:45;
hence  |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]| by A4, A5, EUCLID_8:55; ::_thesis: verum
end;

definition
let f be PartFunc of (REAL 3),REAL;
let p be Element of REAL 3;
func grad (f,p) ->  Element of REAL 3 equals :: PDIFF_4:def 7
(((partdiff (f,p,1)) * <e1>) + ((partdiff (f,p,2)) * <e2>)) + ((partdiff (f,p,3)) * <e3>);
coherence
 (((partdiff (f,p,1)) * <e1>) + ((partdiff (f,p,2)) * <e2>)) + ((partdiff (f,p,3)) * <e3>) is Element of REAL 3 ;
end;

:: deftheorem  defines grad PDIFF_4:def_7_:_
 for f being PartFunc of (REAL 3),REAL
for p being Element of REAL 3 holds grad (f,p) = (((partdiff (f,p,1)) * <e1>) + ((partdiff (f,p,2)) * <e2>)) + ((partdiff (f,p,3)) * <e3>);

theorem Th34: :: PDIFF_4:34
for p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL holds grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]|
proof
let p be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL holds grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]|
let f be PartFunc of (REAL 3),REAL; ::_thesis: grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]|
grad (f,p) = (|[((partdiff (f,p,1)) * 1),((partdiff (f,p,1)) * 0),((partdiff (f,p,1)) * 0)]| + ((partdiff (f,p,2)) * |[0,1,0]|)) + ((partdiff (f,p,3)) * |[0,0,1]|) by EUCLID_8:59
.= (|[(partdiff (f,p,1)),0,0]| + |[((partdiff (f,p,2)) * 0),((partdiff (f,p,2)) * 1),((partdiff (f,p,2)) * 0)]|) + ((partdiff (f,p,3)) * |[0,0,1]|) by EUCLID_8:59
.= (|[(partdiff (f,p,1)),0,0]| + |[0,(partdiff (f,p,2)),0]|) + |[((partdiff (f,p,3)) * 0),((partdiff (f,p,3)) * 0),((partdiff (f,p,3)) * 1)]| by EUCLID_8:59
.= |[((partdiff (f,p,1)) + 0),(0 + (partdiff (f,p,2))),(0 + 0)]| + |[0,0,(partdiff (f,p,3))]| by Lm4
.= |[((partdiff (f,p,1)) + 0),((partdiff (f,p,2)) + 0),(0 + (partdiff (f,p,3)))]| by Lm4
.= |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]| ;
hence  grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]| ; ::_thesis: verum
end;

theorem Th35: :: PDIFF_4:35
for p being Element of REAL 3
for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad ((f + g),p) = (grad (f,p)) + (grad (g,p))
proof
let p be Element of REAL 3; ::_thesis: for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad ((f + g),p) = (grad (f,p)) + (grad (g,p))
let f, g be PartFunc of (REAL 3),REAL; ::_thesis: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 implies grad ((f + g),p) = (grad (f,p)) + (grad (g,p)) )
assume that
A1: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 ) and
A2: ( g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 ) ; ::_thesis: grad ((f + g),p) = (grad (f,p)) + (grad (g,p))
grad ((f + g),p) = |[(partdiff ((f + g),p,1)),(partdiff ((f + g),p,2)),(partdiff ((f + g),p,3))]| by Th34
.= |[((partdiff (f,p,1)) + (partdiff (g,p,1))),(partdiff ((f + g),p,2)),(partdiff ((f + g),p,3))]| by A1, A2, PDIFF_1:29
.= |[((partdiff (f,p,1)) + (partdiff (g,p,1))),((partdiff (f,p,2)) + (partdiff (g,p,2))),(partdiff ((f + g),p,3))]| by A1, A2, PDIFF_1:29
.= |[((partdiff (f,p,1)) + (partdiff (g,p,1))),((partdiff (f,p,2)) + (partdiff (g,p,2))),((partdiff (f,p,3)) + (partdiff (g,p,3)))]| by A1, A2, PDIFF_1:29
.= |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]| + |[(partdiff (g,p,1)),(partdiff (g,p,2)),(partdiff (g,p,3))]| by Lm4
.= (grad (f,p)) + |[(partdiff (g,p,1)),(partdiff (g,p,2)),(partdiff (g,p,3))]| by Th34
.= (grad (f,p)) + (grad (g,p)) by Th34 ;
hence  grad ((f + g),p) = (grad (f,p)) + (grad (g,p)) ; ::_thesis: verum
end;

theorem Th36: :: PDIFF_4:36
for p being Element of REAL 3
for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad ((f - g),p) = (grad (f,p)) - (grad (g,p))
proof
let p be Element of REAL 3; ::_thesis: for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad ((f - g),p) = (grad (f,p)) - (grad (g,p))
let f, g be PartFunc of (REAL 3),REAL; ::_thesis: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 implies grad ((f - g),p) = (grad (f,p)) - (grad (g,p)) )
assume that
A1: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 ) and
A2: ( g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 ) ; ::_thesis: grad ((f - g),p) = (grad (f,p)) - (grad (g,p))
grad ((f - g),p) = |[(partdiff ((f - g),p,1)),(partdiff ((f - g),p,2)),(partdiff ((f - g),p,3))]| by Th34
.= |[((partdiff (f,p,1)) - (partdiff (g,p,1))),(partdiff ((f - g),p,2)),(partdiff ((f - g),p,3))]| by A1, A2, PDIFF_1:31
.= |[((partdiff (f,p,1)) - (partdiff (g,p,1))),((partdiff (f,p,2)) - (partdiff (g,p,2))),(partdiff ((f - g),p,3))]| by A1, A2, PDIFF_1:31
.= |[((partdiff (f,p,1)) - (partdiff (g,p,1))),((partdiff (f,p,2)) - (partdiff (g,p,2))),((partdiff (f,p,3)) - (partdiff (g,p,3)))]| by A1, A2, PDIFF_1:31
.= |[((partdiff (f,p,1)) + (- (partdiff (g,p,1)))),((partdiff (f,p,2)) + (- (partdiff (g,p,2)))),((partdiff (f,p,3)) + (- (partdiff (g,p,3))))]|
.= |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]| + |[(- (partdiff (g,p,1))),(- (partdiff (g,p,2))),(- (partdiff (g,p,3)))]| by Lm4
.= (grad (f,p)) + |[((- 1) * (partdiff (g,p,1))),((- 1) * (partdiff (g,p,2))),((- 1) * (partdiff (g,p,3)))]| by Th34
.= (grad (f,p)) + ((- 1) * |[(partdiff (g,p,1)),(partdiff (g,p,2)),(partdiff (g,p,3))]|) by EUCLID_8:59
.= (grad (f,p)) - (grad (g,p)) by Th34 ;
hence  grad ((f - g),p) = (grad (f,p)) - (grad (g,p)) ; ::_thesis: verum
end;

theorem Th37: :: PDIFF_4:37
for r being Real
for p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 holds
grad ((r (#) f),p) = r * (grad (f,p))
proof
let r be Real; ::_thesis: for p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 holds
grad ((r (#) f),p) = r * (grad (f,p))
let p be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 holds
grad ((r (#) f),p) = r * (grad (f,p))
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 implies grad ((r (#) f),p) = r * (grad (f,p)) )
assume A1: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 ) ; ::_thesis: grad ((r (#) f),p) = r * (grad (f,p))
grad ((r (#) f),p) = |[(partdiff ((r (#) f),p,1)),(partdiff ((r (#) f),p,2)),(partdiff ((r (#) f),p,3))]| by Th34
.= |[(r * (partdiff (f,p,1))),(partdiff ((r (#) f),p,2)),(partdiff ((r (#) f),p,3))]| by A1, PDIFF_1:33
.= |[(r * (partdiff (f,p,1))),(r * (partdiff (f,p,2))),(partdiff ((r (#) f),p,3))]| by A1, PDIFF_1:33
.= |[(r * (partdiff (f,p,1))),(r * (partdiff (f,p,2))),(r * (partdiff (f,p,3)))]| by A1, PDIFF_1:33
.= r * |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]| by EUCLID_8:59
.= r * (grad (f,p)) by Th34 ;
hence  grad ((r (#) f),p) = r * (grad (f,p)) ; ::_thesis: verum
end;

theorem :: PDIFF_4:38
for s, t being Real
for p being Element of REAL 3
for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad (((s (#) f) + (t (#) g)),p) = (s * (grad (f,p))) + (t * (grad (g,p)))
proof
let s, t be Real; ::_thesis: for p being Element of REAL 3
for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad (((s (#) f) + (t (#) g)),p) = (s * (grad (f,p))) + (t * (grad (g,p)))
let p be Element of REAL 3; ::_thesis: for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad (((s (#) f) + (t (#) g)),p) = (s * (grad (f,p))) + (t * (grad (g,p)))
let f, g be PartFunc of (REAL 3),REAL; ::_thesis: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 implies grad (((s (#) f) + (t (#) g)),p) = (s * (grad (f,p))) + (t * (grad (g,p))) )
assume that
A1: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 ) and
A2: ( g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 ) ; ::_thesis: grad (((s (#) f) + (t (#) g)),p) = (s * (grad (f,p))) + (t * (grad (g,p)))
A3: ( s (#) f is_partial_differentiable_in p,1 & s (#) f is_partial_differentiable_in p,2 & s (#) f is_partial_differentiable_in p,3 ) by A1, PDIFF_1:33;
 ( t (#) g is_partial_differentiable_in p,1 & t (#) g is_partial_differentiable_in p,2 & t (#) g is_partial_differentiable_in p,3 ) by A2, PDIFF_1:33;
then  grad (((s (#) f) + (t (#) g)),p) = (grad ((s (#) f),p)) + (grad ((t (#) g),p)) by A3, Th35
.= (s * (grad (f,p))) + (grad ((t (#) g),p)) by A1, Th37
.= (s * (grad (f,p))) + (t * (grad (g,p))) by A2, Th37 ;
hence  grad (((s (#) f) + (t (#) g)),p) = (s * (grad (f,p))) + (t * (grad (g,p))) ; ::_thesis: verum
end;

theorem :: PDIFF_4:39
for s, t being Real
for p being Element of REAL 3
for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad (((s (#) f) - (t (#) g)),p) = (s * (grad (f,p))) - (t * (grad (g,p)))
proof
let s, t be Real; ::_thesis: for p being Element of REAL 3
for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad (((s (#) f) - (t (#) g)),p) = (s * (grad (f,p))) - (t * (grad (g,p)))
let p be Element of REAL 3; ::_thesis: for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad (((s (#) f) - (t (#) g)),p) = (s * (grad (f,p))) - (t * (grad (g,p)))
let f, g be PartFunc of (REAL 3),REAL; ::_thesis: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 implies grad (((s (#) f) - (t (#) g)),p) = (s * (grad (f,p))) - (t * (grad (g,p))) )
assume that
A1: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 ) and
A2: ( g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 ) ; ::_thesis: grad (((s (#) f) - (t (#) g)),p) = (s * (grad (f,p))) - (t * (grad (g,p)))
A3: ( s (#) f is_partial_differentiable_in p,1 & s (#) f is_partial_differentiable_in p,2 & s (#) f is_partial_differentiable_in p,3 ) by A1, PDIFF_1:33;
 ( t (#) g is_partial_differentiable_in p,1 & t (#) g is_partial_differentiable_in p,2 & t (#) g is_partial_differentiable_in p,3 ) by A2, PDIFF_1:33;
then  grad (((s (#) f) - (t (#) g)),p) = (grad ((s (#) f),p)) - (grad ((t (#) g),p)) by A3, Th36
.= (s * (grad (f,p))) - (grad ((t (#) g),p)) by A1, Th37
.= (s * (grad (f,p))) - (t * (grad (g,p))) by A2, Th37 ;
hence  grad (((s (#) f) - (t (#) g)),p) = (s * (grad (f,p))) - (t * (grad (g,p))) ; ::_thesis: verum
end;

theorem :: PDIFF_4:40
for p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st f is total & f is constant holds
grad (f,p) = 0.REAL 3
proof
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 A1: ( 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 A1, A2, PARTFUN2:def_1;
now__::_thesis:_for_x_being_Real_st_x_in_dom_(f_*_(reproj_(1,p)))_holds_
(f_*_(reproj_(1,p)))_._x_=_a
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:12;
hence  (f * (reproj (1,p))) . x = a by A3; ::_thesis: verum
end;
then A4: f * (reproj (1,p)) is constant by PARTFUN2:def_1;
set g1 = f * (reproj (1,p));
A5: dom (f * (reproj (1,p))) = W by A1, FUNCT_2:def_1;
A6: (f * (reproj (1,p))) | W is constant by A4;
then A7: f * (reproj (1,p)) is_differentiable_on REAL by A5, FDIFF_1:22;
 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 A7, FDIFF_1:def_7
.= 0 by A5, A6, FDIFF_1:22 ;
hence  diff ((f * (reproj (1,p))),x) = 0 ; ::_thesis: verum
end;
then A8: partdiff (f,p,1) = 0 ;
now__::_thesis:_for_y_being_Real_st_y_in_dom_(f_*_(reproj_(2,p)))_holds_
(f_*_(reproj_(2,p)))_._y_=_a
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:12;
hence  (f * (reproj (2,p))) . y = a by A3; ::_thesis: verum
end;
then A9: f * (reproj (2,p)) is constant by PARTFUN2:def_1;
set g2 = f * (reproj (2,p));
A10: dom (f * (reproj (2,p))) = W by A1, FUNCT_2:def_1;
A11: (f * (reproj (2,p))) | W is constant by A9;
then A12: ( 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 A10, FDIFF_1:22;
 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 A12, FDIFF_1:def_7
.= 0 by A10, A11, FDIFF_1:22 ;
hence  diff ((f * (reproj (2,p))),y) = 0 ; ::_thesis: verum
end;
then A13: partdiff (f,p,2) = 0 ;
now__::_thesis:_for_z_being_Real_st_z_in_dom_(f_*_(reproj_(3,p)))_holds_
(f_*_(reproj_(3,p)))_._z_=_a
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:12;
hence  (f * (reproj (3,p))) . z = a by A3; ::_thesis: verum
end;
then A14: f * (reproj (3,p)) is constant by PARTFUN2:def_1;
set g3 = f * (reproj (3,p));
A15: dom (f * (reproj (3,p))) = W by A1, FUNCT_2:def_1;
A16: (f * (reproj (3,p))) | W is constant by A14;
then A17: ( 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 A15, FDIFF_1:22;
 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 A17, FDIFF_1:def_7
.= 0 by A15, A16, FDIFF_1:22 ;
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 A8, A13, Th34
.= 0.REAL 3 by FINSEQ_2:62 ;
hence  grad (f,p) = 0.REAL 3 ; ::_thesis: verum
end;

definition
let a be Element of REAL 3;
func unitvector a ->  Element of REAL 3 equals :: PDIFF_4:def 8
|[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]|;
coherence
 |[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]| is Element of REAL 3 ;
end;

:: deftheorem  defines unitvector PDIFF_4:def_8_:_
 for a being Element of REAL 3 holds unitvector a = |[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]|;

definition
let f be PartFunc of (REAL 3),REAL;
let p, a be Element of REAL 3;
func Directiondiff (f,p,a) ->  Real equals :: PDIFF_4:def 9
(((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3));
coherence
 (((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3)) is Real ;
end;

:: deftheorem  defines Directiondiff PDIFF_4:def_9_:_
 for f being PartFunc of (REAL 3),REAL
for p, a being Element of REAL 3 holds Directiondiff (f,p,a) = (((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3));

theorem :: PDIFF_4:41
for x0, y0, z0 being Real
for a, p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st a = <*x0,y0,z0*> holds
Directiondiff (f,p,a) = ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * y0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))) + (((partdiff (f,p,3)) * z0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))
proof
let x0, y0, z0 be Real; ::_thesis: for a, p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st a = <*x0,y0,z0*> holds
Directiondiff (f,p,a) = ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * y0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))) + (((partdiff (f,p,3)) * z0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))
let a, p be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL st a = <*x0,y0,z0*> holds
Directiondiff (f,p,a) = ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * y0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))) + (((partdiff (f,p,3)) * z0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))
let f be PartFunc of (REAL 3),REAL; ::_thesis: ( a = <*x0,y0,z0*> implies Directiondiff (f,p,a) = ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * y0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))) + (((partdiff (f,p,3)) * z0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) )
assume A1: a = <*x0,y0,z0*> ; ::_thesis: Directiondiff (f,p,a) = ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * y0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))) + (((partdiff (f,p,3)) * z0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))
then A2: sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)) = sqrt (((x0 ^2) + ((a . 2) ^2)) + ((a . 3) ^2)) by FINSEQ_1:45
.= sqrt (((x0 ^2) + (y0 ^2)) + ((a . 3) ^2)) by A1, FINSEQ_1:45
.= sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)) by A1, FINSEQ_1:45 ;
Directiondiff (f,p,a) = (((partdiff (f,p,1)) * ((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3)) by FINSEQ_1:45
.= ((((partdiff (f,p,1)) * (a . 1)) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3)) by XCMPLX_1:74
.= ((((partdiff (f,p,1)) * (a . 1)) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))) + ((partdiff (f,p,2)) * ((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))))) + ((partdiff (f,p,3)) * ((unitvector a) . 3)) by FINSEQ_1:45
.= ((((partdiff (f,p,1)) * (a . 1)) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))) + (((partdiff (f,p,2)) * (a . 2)) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))) + ((partdiff (f,p,3)) * ((unitvector a) . 3)) by XCMPLX_1:74
.= ((((partdiff (f,p,1)) * (a . 1)) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))) + (((partdiff (f,p,2)) * (a . 2)) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))) + ((partdiff (f,p,3)) * ((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))) by FINSEQ_1:45
.= ((((partdiff (f,p,1)) * (a . 1)) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))) + (((partdiff (f,p,2)) * (a . 2)) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))) + (((partdiff (f,p,3)) * (a . 3)) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))) by XCMPLX_1:74
.= ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * (a . 2)) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))) + (((partdiff (f,p,3)) * (a . 3)) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))) by A1, A2, FINSEQ_1:45
.= ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * y0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))) + (((partdiff (f,p,3)) * (a . 3)) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))) by A1, A2, FINSEQ_1:45
.= ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * y0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))) + (((partdiff (f,p,3)) * z0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) by A1, A2, FINSEQ_1:45 ;
hence  Directiondiff (f,p,a) = ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * y0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))) + (((partdiff (f,p,3)) * z0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) ; ::_thesis: verum
end;

theorem :: PDIFF_4:42
for p, a being Element of REAL 3
for f being PartFunc of (REAL 3),REAL holds Directiondiff (f,p,a) = |((grad (f,p)),(unitvector a))|
proof
let p, a be Element of REAL 3; ::_thesis: for f being PartFunc of (REAL 3),REAL holds Directiondiff (f,p,a) = |((grad (f,p)),(unitvector a))|
let f be PartFunc of (REAL 3),REAL; ::_thesis: Directiondiff (f,p,a) = |((grad (f,p)),(unitvector a))|
set p0 = grad (f,p);
reconsider g1 = grad (f,p), g2 = unitvector a as FinSequence of REAL ;
A1: len g1 = len <*((grad (f,p)) . 1),((grad (f,p)) . 2),((grad (f,p)) . 3)*> by EUCLID_8:1
.= 3 by FINSEQ_1:45 ;
A2: len g2 = 3 by FINSEQ_1:45;
A3: grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]| by Th34;
|((grad (f,p)),(unitvector a))| = Sum <*((g1 . 1) * (g2 . 1)),((g1 . 2) * (g2 . 2)),((g1 . 3) * (g2 . 3))*> by A1, A2, EUCLID_5:28
.= ((((grad (f,p)) . 1) * (g2 . 1)) + (((grad (f,p)) . 2) * (g2 . 2))) + (((grad (f,p)) . 3) * (g2 . 3)) by RVSUM_1:78
.= (((partdiff (f,p,1)) * (g2 . 1)) + (((grad (f,p)) . 2) * (g2 . 2))) + (((grad (f,p)) . 3) * (g2 . 3)) by A3, FINSEQ_1:45
.= (((partdiff (f,p,1)) * (g2 . 1)) + ((partdiff (f,p,2)) * (g2 . 2))) + (((grad (f,p)) . 3) * (g2 . 3)) by A3, FINSEQ_1:45
.= Directiondiff (f,p,a) by A3, FINSEQ_1:45 ;
hence  Directiondiff (f,p,a) = |((grad (f,p)),(unitvector a))| ; ::_thesis: verum
end;

definition
let f1, f2, f3 be PartFunc of (REAL 3),REAL;
let p be Element of REAL 3;
func curl (f1,f2,f3,p) ->  Element of REAL 3 equals :: PDIFF_4:def 10
((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * <e1>) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * <e2>)) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * <e3>);
coherence
 ((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * <e1>) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * <e2>)) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * <e3>) is Element of REAL 3 ;
end;

:: deftheorem  defines curl PDIFF_4:def_10_:_
 for f1, f2, f3 being PartFunc of (REAL 3),REAL
for p being Element of REAL 3 holds curl (f1,f2,f3,p) = ((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * <e1>) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * <e2>)) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * <e3>);

theorem :: PDIFF_4:43
for p being Element of REAL 3
for f1, f2, f3 being PartFunc of (REAL 3),REAL holds curl (f1,f2,f3,p) = |[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),((partdiff (f1,p,3)) - (partdiff (f3,p,1))),((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]|
proof
let p be Element of REAL 3; ::_thesis: for f1, f2, f3 being PartFunc of (REAL 3),REAL holds curl (f1,f2,f3,p) = |[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),((partdiff (f1,p,3)) - (partdiff (f3,p,1))),((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]|
let f1, f2, f3 be PartFunc of (REAL 3),REAL; ::_thesis: curl (f1,f2,f3,p) = |[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),((partdiff (f1,p,3)) - (partdiff (f3,p,1))),((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]|
curl (f1,f2,f3,p) = (|[(((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * 1),(((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * 0),(((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * 0)]| + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * |[0,1,0]|)) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * |[0,0,1]|) by EUCLID_8:59
.= (|[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),0,0]| + |[(((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * 0),(((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * 1),(((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * 0)]|) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * |[0,0,1]|) by EUCLID_8:59
.= (|[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),0,0]| + |[0,((partdiff (f1,p,3)) - (partdiff (f3,p,1))),0]|) + |[(((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * 0),(((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * 0),(((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * 1)]| by EUCLID_8:59
.= |[(((partdiff (f3,p,2)) - (partdiff (f2,p,3))) + 0),(0 + ((partdiff (f1,p,3)) - (partdiff (f3,p,1)))),(0 + 0)]| + |[0,0,((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]| by Lm4
.= |[(((partdiff (f3,p,2)) - (partdiff (f2,p,3))) + 0),(((partdiff (f1,p,3)) - (partdiff (f3,p,1))) + 0),(0 + ((partdiff (f2,p,1)) - (partdiff (f1,p,2))))]| by Lm4
.= |[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),((partdiff (f1,p,3)) - (partdiff (f3,p,1))),((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]| ;
hence  curl (f1,f2,f3,p) = |[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),((partdiff (f1,p,3)) - (partdiff (f3,p,1))),((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]| ; ::_thesis: verum
end;