:: PDIFF_2 semantic presentation
begin
theorem Th1: :: PDIFF_2:1
( dom (proj (1,2)) = REAL 2 & rng (proj (1,2)) = REAL & ( for x, y being Element of REAL holds (proj (1,2)) . <*x,y*> = x ) )
proof
set f = proj (1,2);
A1: for x being set st x in REAL holds
ex z being set st
( z in REAL 2 & x = (proj (1,2)) . z )
proof
set y = the Element of REAL ;
let x be set ; ::_thesis: ( x in REAL implies ex z being set st
( z in REAL 2 & x = (proj (1,2)) . z ) )
assume x in REAL ; ::_thesis: ex z being set st
( z in REAL 2 & x = (proj (1,2)) . z )
then reconsider x1 = x as Element of REAL ;
reconsider z = <*x1, the Element of REAL *> as Element of REAL 2 by FINSEQ_2:101;
(proj (1,2)) . z = z . 1 by PDIFF_1:def_1;
then (proj (1,2)) . z = x by FINSEQ_1:44;
hence ex z being set st
( z in REAL 2 & x = (proj (1,2)) . z ) ; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Element_of_REAL_holds_(proj_(1,2))_._<*x,y*>_=_x
let x, y be Element of REAL ; ::_thesis: (proj (1,2)) . <*x,y*> = x
<*x,y*> is Element of 2 -tuples_on REAL by FINSEQ_2:101;
then (proj (1,2)) . <*x,y*> = <*x,y*> . 1 by PDIFF_1:def_1;
hence (proj (1,2)) . <*x,y*> = x by FINSEQ_1:44; ::_thesis: verum
end;
hence ( dom (proj (1,2)) = REAL 2 & rng (proj (1,2)) = REAL & ( for x, y being Element of REAL holds (proj (1,2)) . <*x,y*> = x ) ) by A1, FUNCT_2:10, FUNCT_2:def_1; ::_thesis: verum
end;
theorem Th2: :: PDIFF_2:2
( dom (proj (2,2)) = REAL 2 & rng (proj (2,2)) = REAL & ( for x, y being Element of REAL holds (proj (2,2)) . <*x,y*> = y ) )
proof
set f = proj (2,2);
A1: for y being set st y in REAL holds
ex z being set st
( z in REAL 2 & y = (proj (2,2)) . z )
proof
set x = the Element of REAL ;
let y be set ; ::_thesis: ( y in REAL implies ex z being set st
( z in REAL 2 & y = (proj (2,2)) . z ) )
assume y in REAL ; ::_thesis: ex z being set st
( z in REAL 2 & y = (proj (2,2)) . z )
then reconsider y1 = y as Element of REAL ;
reconsider z = <* the Element of REAL ,y1*> as Element of REAL 2 by FINSEQ_2:101;
(proj (2,2)) . z = z . 2 by PDIFF_1:def_1;
then (proj (2,2)) . z = y by FINSEQ_1:44;
hence ex z being set st
( z in REAL 2 & y = (proj (2,2)) . z ) ; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Element_of_REAL_holds_(proj_(2,2))_._<*x,y*>_=_y
let x, y be Element of REAL ; ::_thesis: (proj (2,2)) . <*x,y*> = y
<*x,y*> is Element of 2 -tuples_on REAL by FINSEQ_2:101;
then (proj (2,2)) . <*x,y*> = <*x,y*> . 2 by PDIFF_1:def_1;
hence (proj (2,2)) . <*x,y*> = y by FINSEQ_1:44; ::_thesis: verum
end;
hence ( dom (proj (2,2)) = REAL 2 & rng (proj (2,2)) = REAL & ( for x, y being Element of REAL holds (proj (2,2)) . <*x,y*> = y ) ) by A1, FUNCT_2:10, FUNCT_2:def_1; ::_thesis: verum
end;
begin
definition
let n, i be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let z be Element of REAL n;
func SVF1 (i,f,z) -> PartFunc of REAL,REAL equals :: PDIFF_2:def 1
f * (reproj (i,z));
coherence
f * (reproj (i,z)) is PartFunc of REAL,REAL ;
end;
:: deftheorem defines SVF1 PDIFF_2:def_1_:_
for n, i being Element of NAT
for f being PartFunc of (REAL n),REAL
for z being Element of REAL n holds SVF1 (i,f,z) = f * (reproj (i,z));
theorem Th3: :: PDIFF_2:3
for x, y being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x,y*> & f is_partial_differentiable_in z,1 holds
SVF1 (1,f,z) is_differentiable_in x
proof
let x, y be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x,y*> & f is_partial_differentiable_in z,1 holds
SVF1 (1,f,z) is_differentiable_in x
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x,y*> & f is_partial_differentiable_in z,1 holds
SVF1 (1,f,z) is_differentiable_in x
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x,y*> & f is_partial_differentiable_in z,1 implies SVF1 (1,f,z) is_differentiable_in x )
assume that
A1: z = <*x,y*> and
A2: f is_partial_differentiable_in z,1 ; ::_thesis: SVF1 (1,f,z) is_differentiable_in x
(proj (1,2)) . z = x by A1, Th1;
hence SVF1 (1,f,z) is_differentiable_in x by A2, PDIFF_1:def_11; ::_thesis: verum
end;
theorem Th4: :: PDIFF_2:4
for x, y being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x,y*> & f is_partial_differentiable_in z,2 holds
SVF1 (2,f,z) is_differentiable_in y
proof
let x, y be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x,y*> & f is_partial_differentiable_in z,2 holds
SVF1 (2,f,z) is_differentiable_in y
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x,y*> & f is_partial_differentiable_in z,2 holds
SVF1 (2,f,z) is_differentiable_in y
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x,y*> & f is_partial_differentiable_in z,2 implies SVF1 (2,f,z) is_differentiable_in y )
assume that
A1: z = <*x,y*> and
A2: f is_partial_differentiable_in z,2 ; ::_thesis: SVF1 (2,f,z) is_differentiable_in y
(proj (2,2)) . z = y by A1, Th2;
hence SVF1 (2,f,z) is_differentiable_in y by A2, PDIFF_1:def_11; ::_thesis: verum
end;
theorem Th5: :: PDIFF_2:5
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 holds
( ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 (1,f,z) is_differentiable_in x0 ) iff f is_partial_differentiable_in z,1 )
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z being Element of REAL 2 holds
( ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 (1,f,z) is_differentiable_in x0 ) iff f is_partial_differentiable_in z,1 )
let z be Element of REAL 2; ::_thesis: ( ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 (1,f,z) is_differentiable_in x0 ) iff f is_partial_differentiable_in z,1 )
consider x0, y0 being Real such that
A1: z = <*x0,y0*> by FINSEQ_2:100;
hereby ::_thesis: ( f is_partial_differentiable_in z,1 implies ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 (1,f,z) is_differentiable_in x0 ) )
given x0, y0 being Real such that A2: z = <*x0,y0*> and
A3: SVF1 (1,f,z) is_differentiable_in x0 ; ::_thesis: f is_partial_differentiable_in z,1
(proj (1,2)) . z = x0 by A2, Th1;
hence f is_partial_differentiable_in z,1 by A3, PDIFF_1:def_11; ::_thesis: verum
end;
assume A4: f is_partial_differentiable_in z,1 ; ::_thesis: ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 (1,f,z) is_differentiable_in x0 )
(proj (1,2)) . z = x0 by A1, Th1;
then SVF1 (1,f,z) is_differentiable_in x0 by A4, PDIFF_1:def_11;
hence ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 (1,f,z) is_differentiable_in x0 ) by A1; ::_thesis: verum
end;
theorem Th6: :: PDIFF_2:6
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 holds
( ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 (2,f,z) is_differentiable_in y0 ) iff f is_partial_differentiable_in z,2 )
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z being Element of REAL 2 holds
( ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 (2,f,z) is_differentiable_in y0 ) iff f is_partial_differentiable_in z,2 )
let z be Element of REAL 2; ::_thesis: ( ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 (2,f,z) is_differentiable_in y0 ) iff f is_partial_differentiable_in z,2 )
consider x0, y0 being Real such that
A1: z = <*x0,y0*> by FINSEQ_2:100;
hereby ::_thesis: ( f is_partial_differentiable_in z,2 implies ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 (2,f,z) is_differentiable_in y0 ) )
given x0, y0 being Real such that A2: z = <*x0,y0*> and
A3: SVF1 (2,f,z) is_differentiable_in y0 ; ::_thesis: f is_partial_differentiable_in z,2
(proj (2,2)) . z = y0 by A2, Th2;
hence f is_partial_differentiable_in z,2 by A3, PDIFF_1:def_11; ::_thesis: verum
end;
assume A4: f is_partial_differentiable_in z,2 ; ::_thesis: ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 (2,f,z) is_differentiable_in y0 )
(proj (2,2)) . z = y0 by A1, Th2;
then SVF1 (2,f,z) is_differentiable_in y0 by A4, PDIFF_1:def_11;
hence ex x0, y0 being Real st
( z = <*x0,y0*> & SVF1 (2,f,z) is_differentiable_in y0 ) by A1; ::_thesis: verum
end;
theorem :: PDIFF_2:7
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
proof
let x0, y0 be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_partial_differentiable_in z,1 implies ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) )
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,1 ; ::_thesis: ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
ex x1, y1 being Real st
( z = <*x1,y1*> & SVF1 (1,f,z) is_differentiable_in x1 ) by A2, Th5;
then SVF1 (1,f,z) is_differentiable_in x0 by A1, FINSEQ_1:77;
hence ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by FDIFF_1:def_4; ::_thesis: verum
end;
theorem :: PDIFF_2:8
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
proof
let x0, y0 be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_partial_differentiable_in z,2 implies ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) )
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,2 ; ::_thesis: ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
ex x1, y1 being Real st
( z = <*x1,y1*> & SVF1 (2,f,z) is_differentiable_in y1 ) by A2, Th6;
then SVF1 (2,f,z) is_differentiable_in y0 by A1, FINSEQ_1:77;
hence ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by FDIFF_1:def_4; ::_thesis: verum
end;
theorem Th9: :: PDIFF_2:9
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 holds
( f is_partial_differentiable_in z,1 iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z being Element of REAL 2 holds
( f is_partial_differentiable_in z,1 iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
let z be Element of REAL 2; ::_thesis: ( f is_partial_differentiable_in z,1 iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
hereby ::_thesis: ( ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) implies f is_partial_differentiable_in z,1 )
assume A1: f is_partial_differentiable_in z,1 ; ::_thesis: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) )
thus ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ::_thesis: verum
proof
consider x0, y0 being Real such that
A2: z = <*x0,y0*> and
A3: SVF1 (1,f,z) is_differentiable_in x0 by A1, Th5;
ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A3, FDIFF_1:def_4;
hence ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A2; ::_thesis: verum
end;
end;
assume ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ; ::_thesis: f is_partial_differentiable_in z,1
then consider x0, y0 being Real such that
A4: z = <*x0,y0*> and
A5: ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ;
SVF1 (1,f,z) is_differentiable_in x0 by A5, FDIFF_1:def_4;
hence f is_partial_differentiable_in z,1 by A4, Th5; ::_thesis: verum
end;
theorem Th10: :: PDIFF_2:10
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 holds
( f is_partial_differentiable_in z,2 iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z being Element of REAL 2 holds
( f is_partial_differentiable_in z,2 iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )
let z be Element of REAL 2; ::_thesis: ( f is_partial_differentiable_in z,2 iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )
hereby ::_thesis: ( ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) implies f is_partial_differentiable_in z,2 )
assume A1: f is_partial_differentiable_in z,2 ; ::_thesis: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) )
thus ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ::_thesis: verum
proof
consider x0, y0 being Real such that
A2: z = <*x0,y0*> and
A3: SVF1 (2,f,z) is_differentiable_in y0 by A1, Th6;
ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A3, FDIFF_1:def_4;
hence ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by A2; ::_thesis: verum
end;
end;
assume ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ; ::_thesis: f is_partial_differentiable_in z,2
then consider x0, y0 being Real such that
A4: z = <*x0,y0*> and
A5: ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ;
SVF1 (2,f,z) is_differentiable_in y0 by A5, FDIFF_1:def_4;
hence f is_partial_differentiable_in z,2 by A4, Th6; ::_thesis: verum
end;
Lm1: for x0, y0, r being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
( r = diff ((SVF1 (1,f,z)),x0) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
proof
let x0, y0, r be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
( r = diff ((SVF1 (1,f,z)),x0) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
( r = diff ((SVF1 (1,f,z)),x0) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_partial_differentiable_in z,1 implies ( r = diff ((SVF1 (1,f,z)),x0) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ) )
set F1 = SVF1 (1,f,z);
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,1 ; ::_thesis: ( r = diff ((SVF1 (1,f,z)),x0) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
A3: SVF1 (1,f,z) is_differentiable_in x0 by A1, A2, Th3;
hereby ::_thesis: ( ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) implies r = diff ((SVF1 (1,f,z)),x0) )
assume A4: r = diff ((SVF1 (1,f,z)),x0) ; ::_thesis: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
SVF1 (1,f,z) is_differentiable_in x0 by A1, A2, Th3;
then ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) by A4, FDIFF_1:def_5;
hence ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) by A1; ::_thesis: verum
end;
given x1, y1 being Real such that A5: z = <*x1,y1*> and
A6: ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) ) ; ::_thesis: r = diff ((SVF1 (1,f,z)),x0)
x1 = x0 by A1, A5, FINSEQ_1:77;
hence r = diff ((SVF1 (1,f,z)),x0) by A6, A3, FDIFF_1:def_5; ::_thesis: verum
end;
Lm2: for x0, y0, r being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
( r = diff ((SVF1 (2,f,z)),y0) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
proof
let x0, y0, r be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
( r = diff ((SVF1 (2,f,z)),y0) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
( r = diff ((SVF1 (2,f,z)),y0) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_partial_differentiable_in z,2 implies ( r = diff ((SVF1 (2,f,z)),y0) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ) )
set F1 = SVF1 (2,f,z);
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,2 ; ::_thesis: ( r = diff ((SVF1 (2,f,z)),y0) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
A3: SVF1 (2,f,z) is_differentiable_in y0 by A1, A2, Th4;
hereby ::_thesis: ( ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) implies r = diff ((SVF1 (2,f,z)),y0) )
assume A4: r = diff ((SVF1 (2,f,z)),y0) ; ::_thesis: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
SVF1 (2,f,z) is_differentiable_in y0 by A1, A2, Th4;
then ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) by A4, FDIFF_1:def_5;
hence ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) by A1; ::_thesis: verum
end;
given x1, y1 being Real such that A5: z = <*x1,y1*> and
A6: ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) ) ; ::_thesis: r = diff ((SVF1 (2,f,z)),y0)
y1 = y0 by A1, A5, FINSEQ_1:77;
hence r = diff ((SVF1 (2,f,z)),y0) by A6, A3, FDIFF_1:def_5; ::_thesis: verum
end;
theorem Th11: :: PDIFF_2:11
for x0, y0, r being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
( r = partdiff (f,z,1) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
proof
let x0, y0, r be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
( r = partdiff (f,z,1) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
( r = partdiff (f,z,1) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_partial_differentiable_in z,1 implies ( r = partdiff (f,z,1) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ) )
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,1 ; ::_thesis: ( r = partdiff (f,z,1) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )
hereby ::_thesis: ( ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) implies r = partdiff (f,z,1) )
assume r = partdiff (f,z,1) ; ::_thesis: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
then r = diff ((SVF1 (1,f,z)),x0) by A1, Th1;
hence ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) by A1, A2, Lm1; ::_thesis: verum
end;
given x1, y1 being Real such that A3: ( z = <*x1,y1*> & ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) ) ) ; ::_thesis: r = partdiff (f,z,1)
r = diff ((SVF1 (1,f,z)),x0) by A1, A2, A3, Lm1;
hence r = partdiff (f,z,1) by A1, Th1; ::_thesis: verum
end;
theorem Th12: :: PDIFF_2:12
for x0, y0, r being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
( r = partdiff (f,z,2) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
proof
let x0, y0, r be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
( r = partdiff (f,z,2) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
( r = partdiff (f,z,2) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_partial_differentiable_in z,2 implies ( r = partdiff (f,z,2) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ) )
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,2 ; ::_thesis: ( r = partdiff (f,z,2) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )
hereby ::_thesis: ( ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) implies r = partdiff (f,z,2) )
assume r = partdiff (f,z,2) ; ::_thesis: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
then r = diff ((SVF1 (2,f,z)),y0) by A1, Th2;
hence ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) by A1, A2, Lm2; ::_thesis: verum
end;
given x1, y1 being Real such that A3: ( z = <*x1,y1*> & ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) ) ) ; ::_thesis: r = partdiff (f,z,2)
r = diff ((SVF1 (2,f,z)),y0) by A1, A2, A3, Lm2;
hence r = partdiff (f,z,2) by A1, Th2; ::_thesis: verum
end;
theorem :: PDIFF_2:13
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0)
proof
let x0, y0 be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0)
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0)
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_partial_differentiable_in z,1 implies partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0) )
set r = partdiff (f,z,1);
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,1 ; ::_thesis: partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0)
consider x1, y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( partdiff (f,z,1) = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) ) by A1, A2, Th11;
x0 = x1 by A1, A3, FINSEQ_1:77;
then consider N being Neighbourhood of x0 such that
N c= dom (SVF1 (1,f,z)) and
A5: ex L being LinearFunc ex R being RestFunc st
( partdiff (f,z,1) = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A4;
consider L being LinearFunc, R being RestFunc such that
A6: partdiff (f,z,1) = L . 1 and
A7: for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5;
consider r1 being Real such that
A8: for p being Real holds L . p = r1 * p by FDIFF_1:def_3;
A9: partdiff (f,z,1) = r1 * 1 by A6, A8;
consider x2, y2 being Real such that
A10: z = <*x2,y2*> and
A11: SVF1 (1,f,z) is_differentiable_in x2 by A2, Th5;
consider N1 being Neighbourhood of x2 such that
N1 c= dom (SVF1 (1,f,z)) and
A12: ex L being LinearFunc ex R being RestFunc st
( diff ((SVF1 (1,f,z)),x2) = L . 1 & ( for x being Real st x in N1 holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x2) = (L . (x - x2)) + (R . (x - x2)) ) ) by A11, FDIFF_1:def_5;
consider L1 being LinearFunc, R1 being RestFunc such that
A13: diff ((SVF1 (1,f,z)),x2) = L1 . 1 and
A14: for x being Real st x in N1 holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x2) = (L1 . (x - x2)) + (R1 . (x - x2)) by A12;
consider p1 being Real such that
A15: for p being Real holds L1 . p = p1 * p by FDIFF_1:def_3;
A16: x0 = x2 by A1, A10, FINSEQ_1:77;
then consider N0 being Neighbourhood of x0 such that
A17: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17;
consider g being real number such that
A18: 0 < g and
A19: N0 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6;
deffunc H1( Element of NAT ) -> Element of REAL = g / ($1 + 2);
consider s1 being Real_Sequence such that
A20: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0
let n be Element of NAT ; ::_thesis: s1 . n <> 0
g / (n + 2) <> 0 by A18, XREAL_1:139;
hence s1 . n <> 0 by A20; ::_thesis: verum
end;
then A21: s1 is non-zero by SEQ_1:5;
( s1 is convergent & lim s1 = 0 ) by A20, SEQ_4:31;
then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A21, FDIFF_1:def_1;
A22: for n being Element of NAT ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
proof
let n be Element of NAT ; ::_thesis: ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
take x0 + (g / (n + 2)) ; ::_thesis: ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 )
0 + 1 < (n + 1) + 1 by XREAL_1:6;
then g / (n + 2) < g / 1 by A18, XREAL_1:76;
then A23: x0 + (g / (n + 2)) < x0 + g by XREAL_1:6;
g / (n + 2) > 0 by A18, XREAL_1:139;
then x0 + (- g) < x0 + (g / (n + 2)) by A18, XREAL_1:6;
then x0 + (g / (n + 2)) in ].(x0 - g),(x0 + g).[ by A23;
hence ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 ) by A17, A19, A20; ::_thesis: verum
end;
A24: diff ((SVF1 (1,f,z)),x2) = p1 * 1 by A13, A15;
A25: now__::_thesis:_for_x_being_Real_st_x_in_N_&_x_in_N1_holds_
((partdiff_(f,z,1))_*_(x_-_x0))_+_(R_._(x_-_x0))_=_((diff_((SVF1_(1,f,z)),x2))_*_(x_-_x0))_+_(R1_._(x_-_x0))
let x be Real; ::_thesis: ( x in N & x in N1 implies ((partdiff (f,z,1)) * (x - x0)) + (R . (x - x0)) = ((diff ((SVF1 (1,f,z)),x2)) * (x - x0)) + (R1 . (x - x0)) )
assume that
A26: x in N and
A27: x in N1 ; ::_thesis: ((partdiff (f,z,1)) * (x - x0)) + (R . (x - x0)) = ((diff ((SVF1 (1,f,z)),x2)) * (x - x0)) + (R1 . (x - x0))
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A7, A26;
then (L . (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A14, A16, A27;
then (r1 * (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A8;
hence ((partdiff (f,z,1)) * (x - x0)) + (R . (x - x0)) = ((diff ((SVF1 (1,f,z)),x2)) * (x - x0)) + (R1 . (x - x0)) by A15, A9, A24; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Nat_holds_(partdiff_(f,z,1))_-_(diff_((SVF1_(1,f,z)),x2))_=_(((h_")_(#)_(R1_/*_h))_-_((h_")_(#)_(R_/*_h)))_._n
R1 is total by FDIFF_1:def_2;
then dom R1 = REAL by PARTFUN1:def_2;
then A28: rng h c= dom R1 ;
let n be Nat; ::_thesis: (partdiff (f,z,1)) - (diff ((SVF1 (1,f,z)),x2)) = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
R is total by FDIFF_1:def_2;
then dom R = REAL by PARTFUN1:def_2;
then A29: rng h c= dom R ;
A30: n in NAT by ORDINAL1:def_12;
then ex x being Real st
( x in N & x in N1 & h . n = x - x0 ) by A22;
then ((partdiff (f,z,1)) * (h . n)) + (R . (h . n)) = ((diff ((SVF1 (1,f,z)),x2)) * (h . n)) + (R1 . (h . n)) by A25;
then A31: (((partdiff (f,z,1)) * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = (((diff ((SVF1 (1,f,z)),x2)) * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62;
A32: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R /* h) . n) * ((h ") . n) by A30, A29, FUNCT_2:108
.= ((h ") (#) (R /* h)) . n by A30, SEQ_1:8 ;
A33: h . n <> 0 by A30, SEQ_1:5;
A34: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R1 /* h) . n) * ((h ") . n) by A30, A28, FUNCT_2:108
.= ((h ") (#) (R1 /* h)) . n by A30, SEQ_1:8 ;
A35: ((diff ((SVF1 (1,f,z)),x2)) * (h . n)) / (h . n) = (diff ((SVF1 (1,f,z)),x2)) * ((h . n) / (h . n)) by XCMPLX_1:74
.= (diff ((SVF1 (1,f,z)),x2)) * 1 by A33, XCMPLX_1:60
.= diff ((SVF1 (1,f,z)),x2) ;
((partdiff (f,z,1)) * (h . n)) / (h . n) = (partdiff (f,z,1)) * ((h . n) / (h . n)) by XCMPLX_1:74
.= (partdiff (f,z,1)) * 1 by A33, XCMPLX_1:60
.= partdiff (f,z,1) ;
then (partdiff (f,z,1)) + ((R . (h . n)) / (h . n)) = (diff ((SVF1 (1,f,z)),x2)) + ((R1 . (h . n)) / (h . n)) by A31, A35, XCMPLX_1:62;
then partdiff (f,z,1) = (diff ((SVF1 (1,f,z)),x2)) + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A32, A34;
hence (partdiff (f,z,1)) - (diff ((SVF1 (1,f,z)),x2)) = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A30, RFUNCT_2:1; ::_thesis: verum
end;
then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = (partdiff (f,z,1)) - (diff ((SVF1 (1,f,z)),x2)) ) by VALUED_0:def_18;
then A36: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = (partdiff (f,z,1)) - (diff ((SVF1 (1,f,z)),x2)) by SEQ_4:25;
A37: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by FDIFF_1:def_2;
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by FDIFF_1:def_2;
then (partdiff (f,z,1)) - (diff ((SVF1 (1,f,z)),x2)) = 0 - 0 by A36, A37, SEQ_2:12;
hence partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0) by A1, A10, FINSEQ_1:77; ::_thesis: verum
end;
theorem :: PDIFF_2:14
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
partdiff (f,z,2) = diff ((SVF1 (2,f,z)),y0)
proof
let x0, y0 be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
partdiff (f,z,2) = diff ((SVF1 (2,f,z)),y0)
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
partdiff (f,z,2) = diff ((SVF1 (2,f,z)),y0)
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_partial_differentiable_in z,2 implies partdiff (f,z,2) = diff ((SVF1 (2,f,z)),y0) )
set r = partdiff (f,z,2);
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,2 ; ::_thesis: partdiff (f,z,2) = diff ((SVF1 (2,f,z)),y0)
consider x1, y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,f,z)) & ex L being LinearFunc ex R being RestFunc st
( partdiff (f,z,2) = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) ) by A1, A2, Th12;
y0 = y1 by A1, A3, FINSEQ_1:77;
then consider N being Neighbourhood of y0 such that
N c= dom (SVF1 (2,f,z)) and
A5: ex L being LinearFunc ex R being RestFunc st
( partdiff (f,z,2) = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by A4;
consider L being LinearFunc, R being RestFunc such that
A6: partdiff (f,z,2) = L . 1 and
A7: for y being Real st y in N holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A5;
consider r1 being Real such that
A8: for p being Real holds L . p = r1 * p by FDIFF_1:def_3;
A9: partdiff (f,z,2) = r1 * 1 by A6, A8;
consider x2, y2 being Real such that
A10: z = <*x2,y2*> and
A11: SVF1 (2,f,z) is_differentiable_in y2 by A2, Th6;
consider N1 being Neighbourhood of y2 such that
N1 c= dom (SVF1 (2,f,z)) and
A12: ex L being LinearFunc ex R being RestFunc st
( diff ((SVF1 (2,f,z)),y2) = L . 1 & ( for y being Real st y in N1 holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y2) = (L . (y - y2)) + (R . (y - y2)) ) ) by A11, FDIFF_1:def_5;
consider L1 being LinearFunc, R1 being RestFunc such that
A13: diff ((SVF1 (2,f,z)),y2) = L1 . 1 and
A14: for y being Real st y in N1 holds
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y2) = (L1 . (y - y2)) + (R1 . (y - y2)) by A12;
consider p1 being Real such that
A15: for p being Real holds L1 . p = p1 * p by FDIFF_1:def_3;
A16: y0 = y2 by A1, A10, FINSEQ_1:77;
then consider N0 being Neighbourhood of y0 such that
A17: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17;
consider g being real number such that
A18: 0 < g and
A19: N0 = ].(y0 - g),(y0 + g).[ by RCOMP_1:def_6;
deffunc H1( Element of NAT ) -> Element of REAL = g / ($1 + 2);
consider s1 being Real_Sequence such that
A20: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0
let n be Element of NAT ; ::_thesis: s1 . n <> 0
g / (n + 2) <> 0 by A18, XREAL_1:139;
hence s1 . n <> 0 by A20; ::_thesis: verum
end;
then A21: s1 is non-zero by SEQ_1:5;
( s1 is convergent & lim s1 = 0 ) by A20, SEQ_4:31;
then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A21, FDIFF_1:def_1;
A22: for n being Element of NAT ex y being Real st
( y in N & y in N1 & h . n = y - y0 )
proof
let n be Element of NAT ; ::_thesis: ex y being Real st
( y in N & y in N1 & h . n = y - y0 )
take y0 + (g / (n + 2)) ; ::_thesis: ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 )
0 + 1 < (n + 1) + 1 by XREAL_1:6;
then g / (n + 2) < g / 1 by A18, XREAL_1:76;
then A23: y0 + (g / (n + 2)) < y0 + g by XREAL_1:6;
g / (n + 2) > 0 by A18, XREAL_1:139;
then y0 + (- g) < y0 + (g / (n + 2)) by A18, XREAL_1:6;
then y0 + (g / (n + 2)) in ].(y0 - g),(y0 + g).[ by A23;
hence ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 ) by A17, A19, A20; ::_thesis: verum
end;
A24: diff ((SVF1 (2,f,z)),y2) = p1 * 1 by A13, A15;
A25: now__::_thesis:_for_y_being_Real_st_y_in_N_&_y_in_N1_holds_
((partdiff_(f,z,2))_*_(y_-_y0))_+_(R_._(y_-_y0))_=_((diff_((SVF1_(2,f,z)),y2))_*_(y_-_y0))_+_(R1_._(y_-_y0))
let y be Real; ::_thesis: ( y in N & y in N1 implies ((partdiff (f,z,2)) * (y - y0)) + (R . (y - y0)) = ((diff ((SVF1 (2,f,z)),y2)) * (y - y0)) + (R1 . (y - y0)) )
assume that
A26: y in N and
A27: y in N1 ; ::_thesis: ((partdiff (f,z,2)) * (y - y0)) + (R . (y - y0)) = ((diff ((SVF1 (2,f,z)),y2)) * (y - y0)) + (R1 . (y - y0))
((SVF1 (2,f,z)) . y) - ((SVF1 (2,f,z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A7, A26;
then (L . (y - y0)) + (R . (y - y0)) = (L1 . (y - y0)) + (R1 . (y - y0)) by A14, A16, A27;
then (r1 * (y - y0)) + (R . (y - y0)) = (L1 . (y - y0)) + (R1 . (y - y0)) by A8;
hence ((partdiff (f,z,2)) * (y - y0)) + (R . (y - y0)) = ((diff ((SVF1 (2,f,z)),y2)) * (y - y0)) + (R1 . (y - y0)) by A15, A9, A24; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Nat_holds_(partdiff_(f,z,2))_-_(diff_((SVF1_(2,f,z)),y2))_=_(((h_")_(#)_(R1_/*_h))_-_((h_")_(#)_(R_/*_h)))_._n
R1 is total by FDIFF_1:def_2;
then dom R1 = REAL by PARTFUN1:def_2;
then A28: rng h c= dom R1 ;
let n be Nat; ::_thesis: (partdiff (f,z,2)) - (diff ((SVF1 (2,f,z)),y2)) = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
R is total by FDIFF_1:def_2;
then dom R = REAL by PARTFUN1:def_2;
then A29: rng h c= dom R ;
A30: n in NAT by ORDINAL1:def_12;
then ex y being Real st
( y in N & y in N1 & h . n = y - y0 ) by A22;
then ((partdiff (f,z,2)) * (h . n)) + (R . (h . n)) = ((diff ((SVF1 (2,f,z)),y2)) * (h . n)) + (R1 . (h . n)) by A25;
then A31: (((partdiff (f,z,2)) * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = (((diff ((SVF1 (2,f,z)),y2)) * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62;
A32: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R /* h) . n) * ((h ") . n) by A30, A29, FUNCT_2:108
.= ((h ") (#) (R /* h)) . n by A30, SEQ_1:8 ;
A33: h . n <> 0 by A30, SEQ_1:5;
A34: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R1 /* h) . n) * ((h ") . n) by A30, A28, FUNCT_2:108
.= ((h ") (#) (R1 /* h)) . n by A30, SEQ_1:8 ;
A35: ((diff ((SVF1 (2,f,z)),y2)) * (h . n)) / (h . n) = (diff ((SVF1 (2,f,z)),y2)) * ((h . n) / (h . n)) by XCMPLX_1:74
.= (diff ((SVF1 (2,f,z)),y2)) * 1 by A33, XCMPLX_1:60
.= diff ((SVF1 (2,f,z)),y2) ;
((partdiff (f,z,2)) * (h . n)) / (h . n) = (partdiff (f,z,2)) * ((h . n) / (h . n)) by XCMPLX_1:74
.= (partdiff (f,z,2)) * 1 by A33, XCMPLX_1:60
.= partdiff (f,z,2) ;
then (partdiff (f,z,2)) + ((R . (h . n)) / (h . n)) = (diff ((SVF1 (2,f,z)),y2)) + ((R1 . (h . n)) / (h . n)) by A31, A35, XCMPLX_1:62;
then partdiff (f,z,2) = (diff ((SVF1 (2,f,z)),y2)) + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A32, A34;
hence (partdiff (f,z,2)) - (diff ((SVF1 (2,f,z)),y2)) = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A30, RFUNCT_2:1; ::_thesis: verum
end;
then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = (partdiff (f,z,2)) - (diff ((SVF1 (2,f,z)),y2)) ) by VALUED_0:def_18;
then A36: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = (partdiff (f,z,2)) - (diff ((SVF1 (2,f,z)),y2)) by SEQ_4:25;
A37: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by FDIFF_1:def_2;
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by FDIFF_1:def_2;
then (partdiff (f,z,2)) - (diff ((SVF1 (2,f,z)),y2)) = 0 - 0 by A36, A37, SEQ_2:12;
hence partdiff (f,z,2) = diff ((SVF1 (2,f,z)),y0) by A1, A10, FINSEQ_1:77; ::_thesis: verum
end;
definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
predf is_partial_differentiable`1_on Z means :Def2: :: PDIFF_2:def 2
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_partial_differentiable_in z,1 ) );
predf is_partial_differentiable`2_on Z means :Def3: :: PDIFF_2:def 3
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_partial_differentiable_in z,2 ) );
end;
:: deftheorem Def2 defines is_partial_differentiable`1_on PDIFF_2:def_2_:_
for f being PartFunc of (REAL 2),REAL
for Z being set holds
( f is_partial_differentiable`1_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_partial_differentiable_in z,1 ) ) );
:: deftheorem Def3 defines is_partial_differentiable`2_on PDIFF_2:def_3_:_
for f being PartFunc of (REAL 2),REAL
for Z being set holds
( f is_partial_differentiable`2_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_partial_differentiable_in z,2 ) ) );
theorem :: PDIFF_2:15
for Z being Subset of (REAL 2)
for f being PartFunc of (REAL 2),REAL st f is_partial_differentiable`1_on Z holds
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,1 ) )
proof
let Z be Subset of (REAL 2); ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_partial_differentiable`1_on Z holds
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,1 ) )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_partial_differentiable`1_on Z implies ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,1 ) ) )
set g = f | Z;
assume A1: f is_partial_differentiable`1_on Z ; ::_thesis: ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,1 ) )
hence Z c= dom f by Def2; ::_thesis: for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,1
let z0 be Element of REAL 2; ::_thesis: ( z0 in Z implies f is_partial_differentiable_in z0,1 )
assume z0 in Z ; ::_thesis: f is_partial_differentiable_in z0,1
then f | Z is_partial_differentiable_in z0,1 by A1, Def2;
then consider x0, y0 being Real such that
A2: z0 = <*x0,y0*> and
A3: ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(f | Z),z0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(f | Z),z0)) . x) - ((SVF1 (1,(f | Z),z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by Th9;
consider N being Neighbourhood of x0 such that
A4: N c= dom (SVF1 (1,(f | Z),z0)) and
A5: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(f | Z),z0)) . x) - ((SVF1 (1,(f | Z),z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3;
consider L being LinearFunc, R being RestFunc such that
A6: for x being Real st x in N holds
((SVF1 (1,(f | Z),z0)) . x) - ((SVF1 (1,(f | Z),z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5;
A7: for x being Real st x in N holds
((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0))
proof
let x be Real; ::_thesis: ( x in N implies ((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
A8: for x being Real st x in dom (SVF1 (1,(f | Z),z0)) holds
(SVF1 (1,(f | Z),z0)) . x = (SVF1 (1,f,z0)) . x
proof
let x be Real; ::_thesis: ( x in dom (SVF1 (1,(f | Z),z0)) implies (SVF1 (1,(f | Z),z0)) . x = (SVF1 (1,f,z0)) . x )
assume A9: x in dom (SVF1 (1,(f | Z),z0)) ; ::_thesis: (SVF1 (1,(f | Z),z0)) . x = (SVF1 (1,f,z0)) . x
then A10: x in dom (reproj (1,z0)) by FUNCT_1:11;
A11: (reproj (1,z0)) . x in dom (f | Z) by A9, FUNCT_1:11;
(SVF1 (1,(f | Z),z0)) . x = (f | Z) . ((reproj (1,z0)) . x) by A9, FUNCT_1:12
.= f . ((reproj (1,z0)) . x) by A11, FUNCT_1:47
.= (SVF1 (1,f,z0)) . x by A10, FUNCT_1:13 ;
hence (SVF1 (1,(f | Z),z0)) . x = (SVF1 (1,f,z0)) . x ; ::_thesis: verum
end;
A12: x0 in N by RCOMP_1:16;
assume A13: x in N ; ::_thesis: ((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0))
then (L . (x - x0)) + (R . (x - x0)) = ((SVF1 (1,(f | Z),z0)) . x) - ((SVF1 (1,(f | Z),z0)) . x0) by A6
.= ((SVF1 (1,f,z0)) . x) - ((SVF1 (1,(f | Z),z0)) . x0) by A4, A13, A8
.= ((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) by A4, A8, A12 ;
hence ((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ; ::_thesis: verum
end;
for x being Real st x in dom (SVF1 (1,(f | Z),z0)) holds
x in dom (SVF1 (1,f,z0))
proof
let x be Real; ::_thesis: ( x in dom (SVF1 (1,(f | Z),z0)) implies x in dom (SVF1 (1,f,z0)) )
dom (f | Z) = (dom f) /\ Z by RELAT_1:61;
then A14: dom (f | Z) c= dom f by XBOOLE_1:17;
assume x in dom (SVF1 (1,(f | Z),z0)) ; ::_thesis: x in dom (SVF1 (1,f,z0))
then ( x in dom (reproj (1,z0)) & (reproj (1,z0)) . x in dom (f | Z) ) by FUNCT_1:11;
hence x in dom (SVF1 (1,f,z0)) by A14, FUNCT_1:11; ::_thesis: verum
end;
then for x being set st x in dom (SVF1 (1,(f | Z),z0)) holds
x in dom (SVF1 (1,f,z0)) ;
then dom (SVF1 (1,(f | Z),z0)) c= dom (SVF1 (1,f,z0)) by TARSKI:def_3;
then N c= dom (SVF1 (1,f,z0)) by A4, XBOOLE_1:1;
hence f is_partial_differentiable_in z0,1 by A2, A7, Th9; ::_thesis: verum
end;
theorem :: PDIFF_2:16
for Z being Subset of (REAL 2)
for f being PartFunc of (REAL 2),REAL st f is_partial_differentiable`2_on Z holds
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,2 ) )
proof
let Z be Subset of (REAL 2); ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_partial_differentiable`2_on Z holds
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,2 ) )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_partial_differentiable`2_on Z implies ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,2 ) ) )
set g = f | Z;
assume A1: f is_partial_differentiable`2_on Z ; ::_thesis: ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,2 ) )
hence Z c= dom f by Def3; ::_thesis: for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,2
let z0 be Element of REAL 2; ::_thesis: ( z0 in Z implies f is_partial_differentiable_in z0,2 )
assume z0 in Z ; ::_thesis: f is_partial_differentiable_in z0,2
then f | Z is_partial_differentiable_in z0,2 by A1, Def3;
then consider x0, y0 being Real such that
A2: z0 = <*x0,y0*> and
A3: ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(f | Z),z0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(f | Z),z0)) . y) - ((SVF1 (2,(f | Z),z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by Th10;
consider N being Neighbourhood of y0 such that
A4: N c= dom (SVF1 (2,(f | Z),z0)) and
A5: ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(f | Z),z0)) . y) - ((SVF1 (2,(f | Z),z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A3;
consider L being LinearFunc, R being RestFunc such that
A6: for y being Real st y in N holds
((SVF1 (2,(f | Z),z0)) . y) - ((SVF1 (2,(f | Z),z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A5;
A7: for y being Real st y in N holds
((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) = (L . (y - y0)) + (R . (y - y0))
proof
let y be Real; ::_thesis: ( y in N implies ((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
A8: for y being Real st y in dom (SVF1 (2,(f | Z),z0)) holds
(SVF1 (2,(f | Z),z0)) . y = (SVF1 (2,f,z0)) . y
proof
let y be Real; ::_thesis: ( y in dom (SVF1 (2,(f | Z),z0)) implies (SVF1 (2,(f | Z),z0)) . y = (SVF1 (2,f,z0)) . y )
assume A9: y in dom (SVF1 (2,(f | Z),z0)) ; ::_thesis: (SVF1 (2,(f | Z),z0)) . y = (SVF1 (2,f,z0)) . y
then A10: y in dom (reproj (2,z0)) by FUNCT_1:11;
A11: (reproj (2,z0)) . y in dom (f | Z) by A9, FUNCT_1:11;
(SVF1 (2,(f | Z),z0)) . y = (f | Z) . ((reproj (2,z0)) . y) by A9, FUNCT_1:12
.= f . ((reproj (2,z0)) . y) by A11, FUNCT_1:47
.= (SVF1 (2,f,z0)) . y by A10, FUNCT_1:13 ;
hence (SVF1 (2,(f | Z),z0)) . y = (SVF1 (2,f,z0)) . y ; ::_thesis: verum
end;
A12: y0 in N by RCOMP_1:16;
assume A13: y in N ; ::_thesis: ((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) = (L . (y - y0)) + (R . (y - y0))
then (L . (y - y0)) + (R . (y - y0)) = ((SVF1 (2,(f | Z),z0)) . y) - ((SVF1 (2,(f | Z),z0)) . y0) by A6
.= ((SVF1 (2,f,z0)) . y) - ((SVF1 (2,(f | Z),z0)) . y0) by A4, A13, A8
.= ((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) by A4, A8, A12 ;
hence ((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) ; ::_thesis: verum
end;
for y being Real st y in dom (SVF1 (2,(f | Z),z0)) holds
y in dom (SVF1 (2,f,z0))
proof
let y be Real; ::_thesis: ( y in dom (SVF1 (2,(f | Z),z0)) implies y in dom (SVF1 (2,f,z0)) )
dom (f | Z) = (dom f) /\ Z by RELAT_1:61;
then A14: dom (f | Z) c= dom f by XBOOLE_1:17;
assume y in dom (SVF1 (2,(f | Z),z0)) ; ::_thesis: y in dom (SVF1 (2,f,z0))
then ( y in dom (reproj (2,z0)) & (reproj (2,z0)) . y in dom (f | Z) ) by FUNCT_1:11;
hence y in dom (SVF1 (2,f,z0)) by A14, FUNCT_1:11; ::_thesis: verum
end;
then for y being set st y in dom (SVF1 (2,(f | Z),z0)) holds
y in dom (SVF1 (2,f,z0)) ;
then dom (SVF1 (2,(f | Z),z0)) c= dom (SVF1 (2,f,z0)) by TARSKI:def_3;
then N c= dom (SVF1 (2,f,z0)) by A4, XBOOLE_1:1;
hence f is_partial_differentiable_in z0,2 by A2, A7, Th10; ::_thesis: verum
end;
definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
assume A1: f is_partial_differentiable`1_on Z ;
funcf `partial1| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_2:def 4
( dom it = Z & ( for z being Element of REAL 2 st z in Z holds
it . z = partdiff (f,z,1) ) );
existence
ex b1 being PartFunc of (REAL 2),REAL st
( dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = partdiff (f,z,1) ) )
proof
deffunc H1( Element of REAL 2) -> Element of REAL = partdiff (f,$1,1);
defpred S1[ Element of REAL 2] means $1 in Z;
consider F being PartFunc of (REAL 2),REAL such that
A2: ( ( for z being Element of REAL 2 holds
( z in dom F iff S1[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds
F . z = H1(z) ) ) from SEQ_1:sch_3();
take F ; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = partdiff (f,z,1) ) )
now__::_thesis:_for_y_being_set_st_y_in_Z_holds_
y_in_dom_F
Z c= dom f by A1, Def2;
then A3: Z is Subset of (REAL 2) by XBOOLE_1:1;
let y be set ; ::_thesis: ( y in Z implies y in dom F )
assume y in Z ; ::_thesis: y in dom F
hence y in dom F by A2, A3; ::_thesis: verum
end;
then A4: Z c= dom F by TARSKI:def_3;
for y being set st y in dom F holds
y in Z by A2;
then dom F c= Z by TARSKI:def_3;
hence dom F = Z by A4, XBOOLE_0:def_10; ::_thesis: for z being Element of REAL 2 st z in Z holds
F . z = partdiff (f,z,1)
let z be Element of REAL 2; ::_thesis: ( z in Z implies F . z = partdiff (f,z,1) )
assume z in Z ; ::_thesis: F . z = partdiff (f,z,1)
then z in dom F by A2;
hence F . z = partdiff (f,z,1) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = partdiff (f,z,1) ) & dom b2 = Z & ( for z being Element of REAL 2 st z in Z holds
b2 . z = partdiff (f,z,1) ) holds
b1 = b2
proof
let F, G be PartFunc of (REAL 2),REAL; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = partdiff (f,z,1) ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds
G . z = partdiff (f,z,1) ) implies F = G )
assume that
A5: dom F = Z and
A6: for z being Element of REAL 2 st z in Z holds
F . z = partdiff (f,z,1) and
A7: dom G = Z and
A8: for z being Element of REAL 2 st z in Z holds
G . z = partdiff (f,z,1) ; ::_thesis: F = G
now__::_thesis:_for_z_being_Element_of_REAL_2_st_z_in_dom_F_holds_
F_._z_=_G_._z
let z be Element of REAL 2; ::_thesis: ( z in dom F implies F . z = G . z )
assume A9: z in dom F ; ::_thesis: F . z = G . z
then F . z = partdiff (f,z,1) by A5, A6;
hence F . z = G . z by A5, A8, A9; ::_thesis: verum
end;
hence F = G by A5, A7, PARTFUN1:5; ::_thesis: verum
end;
end;
:: deftheorem defines `partial1| PDIFF_2:def_4_:_
for f being PartFunc of (REAL 2),REAL
for Z being set st f is_partial_differentiable`1_on Z holds
for b3 being PartFunc of (REAL 2),REAL holds
( b3 = f `partial1| Z iff ( dom b3 = Z & ( for z being Element of REAL 2 st z in Z holds
b3 . z = partdiff (f,z,1) ) ) );
definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
assume A1: f is_partial_differentiable`2_on Z ;
funcf `partial2| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_2:def 5
( dom it = Z & ( for z being Element of REAL 2 st z in Z holds
it . z = partdiff (f,z,2) ) );
existence
ex b1 being PartFunc of (REAL 2),REAL st
( dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = partdiff (f,z,2) ) )
proof
deffunc H1( Element of REAL 2) -> Element of REAL = partdiff (f,$1,2);
defpred S1[ Element of REAL 2] means $1 in Z;
consider F being PartFunc of (REAL 2),REAL such that
A2: ( ( for z being Element of REAL 2 holds
( z in dom F iff S1[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds
F . z = H1(z) ) ) from SEQ_1:sch_3();
take F ; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = partdiff (f,z,2) ) )
now__::_thesis:_for_y_being_set_st_y_in_Z_holds_
y_in_dom_F
Z c= dom f by A1, Def3;
then A3: Z is Subset of (REAL 2) by XBOOLE_1:1;
let y be set ; ::_thesis: ( y in Z implies y in dom F )
assume y in Z ; ::_thesis: y in dom F
hence y in dom F by A2, A3; ::_thesis: verum
end;
then A4: Z c= dom F by TARSKI:def_3;
for y being set st y in dom F holds
y in Z by A2;
then dom F c= Z by TARSKI:def_3;
hence dom F = Z by A4, XBOOLE_0:def_10; ::_thesis: for z being Element of REAL 2 st z in Z holds
F . z = partdiff (f,z,2)
let z be Element of REAL 2; ::_thesis: ( z in Z implies F . z = partdiff (f,z,2) )
assume z in Z ; ::_thesis: F . z = partdiff (f,z,2)
then z in dom F by A2;
hence F . z = partdiff (f,z,2) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = partdiff (f,z,2) ) & dom b2 = Z & ( for z being Element of REAL 2 st z in Z holds
b2 . z = partdiff (f,z,2) ) holds
b1 = b2
proof
let F, G be PartFunc of (REAL 2),REAL; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = partdiff (f,z,2) ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds
G . z = partdiff (f,z,2) ) implies F = G )
assume that
A5: dom F = Z and
A6: for z being Element of REAL 2 st z in Z holds
F . z = partdiff (f,z,2) and
A7: dom G = Z and
A8: for z being Element of REAL 2 st z in Z holds
G . z = partdiff (f,z,2) ; ::_thesis: F = G
now__::_thesis:_for_z_being_Element_of_REAL_2_st_z_in_dom_F_holds_
F_._z_=_G_._z
let z be Element of REAL 2; ::_thesis: ( z in dom F implies F . z = G . z )
assume A9: z in dom F ; ::_thesis: F . z = G . z
then F . z = partdiff (f,z,2) by A5, A6;
hence F . z = G . z by A5, A8, A9; ::_thesis: verum
end;
hence F = G by A5, A7, PARTFUN1:5; ::_thesis: verum
end;
end;
:: deftheorem defines `partial2| PDIFF_2:def_5_:_
for f being PartFunc of (REAL 2),REAL
for Z being set st f is_partial_differentiable`2_on Z holds
for b3 being PartFunc of (REAL 2),REAL holds
( b3 = f `partial2| Z iff ( dom b3 = Z & ( for z being Element of REAL 2 st z in Z holds
b3 . z = partdiff (f,z,2) ) ) );
begin
theorem :: PDIFF_2:17
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2
for N being Neighbourhood of (proj (1,2)) . z0 st f is_partial_differentiable_in z0,1 & N c= dom (SVF1 (1,f,z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2
for N being Neighbourhood of (proj (1,2)) . z0 st f is_partial_differentiable_in z0,1 & N c= dom (SVF1 (1,f,z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )
let z0 be Element of REAL 2; ::_thesis: for N being Neighbourhood of (proj (1,2)) . z0 st f is_partial_differentiable_in z0,1 & N c= dom (SVF1 (1,f,z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )
let N be Neighbourhood of (proj (1,2)) . z0; ::_thesis: ( f is_partial_differentiable_in z0,1 & N c= dom (SVF1 (1,f,z0)) implies for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) ) )
assume that
A1: f is_partial_differentiable_in z0,1 and
A2: N c= dom (SVF1 (1,f,z0)) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )
consider x0, y0 being Real such that
A3: z0 = <*x0,y0*> and
A4: ex N1 being Neighbourhood of x0 st
( N1 c= dom (SVF1 (1,f,z0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N1 holds
((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A1, Th9;
consider N1 being Neighbourhood of x0 such that
N1 c= dom (SVF1 (1,f,z0)) and
A5: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N1 holds
((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A4;
A6: (proj (1,2)) . z0 = x0 by A3, Th1;
then consider N2 being Neighbourhood of x0 such that
A7: N2 c= N and
A8: N2 c= N1 by RCOMP_1:17;
A9: N2 c= dom (SVF1 (1,f,z0)) by A2, A7, XBOOLE_1:1;
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )
let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) ) )
assume that
A10: rng c = {((proj (1,2)) . z0)} and
A11: rng (h + c) c= N ; ::_thesis: ( (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent & partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) )
consider g being real number such that
A12: 0 < g and
A13: N2 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6;
( x0 + 0 < x0 + g & x0 - g < x0 - 0 ) by A12, XREAL_1:8, XREAL_1:44;
then A14: x0 in N2 by A13;
A15: rng c c= dom (SVF1 (1,f,z0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in dom (SVF1 (1,f,z0)) )
assume y in rng c ; ::_thesis: y in dom (SVF1 (1,f,z0))
then y = x0 by A10, A6, TARSKI:def_1;
then y in N by A7, A14;
hence y in dom (SVF1 (1,f,z0)) by A2; ::_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 A10, A6, TARSKI:def_1;
then A16: lim c = x0 by SEQ_4:25;
A17: h + c is convergent by SEQ_2:5;
lim h = 0 ;
then lim (h + c) = 0 + x0 by A16, SEQ_2:6
.= x0 ;
then consider n being Element of NAT such that
A18: for m being Element of NAT st n <= m holds
abs (((h + c) . m) - x0) < g by A12, A17, SEQ_2:def_7;
take n ; ::_thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
A19: rng (c ^\ n) = {x0} by A10, A6, VALUED_0:26;
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 A14, A19, 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
A20: y = ((h + c) ^\ n) . m by FUNCT_2:113;
n + 0 <= n + m by XREAL_1:7;
then A21: abs (((h + c) . (n + m)) - x0) < g by A18;
then ((h + c) . (m + n)) - x0 < g by SEQ_2:1;
then (((h + c) ^\ n) . m) - x0 < g by NAT_1:def_3;
then A22: ((h + c) ^\ n) . m < x0 + g by XREAL_1:19;
- g < ((h + c) . (m + n)) - x0 by A21, SEQ_2:1;
then - g < (((h + c) ^\ n) . m) - x0 by NAT_1:def_3;
then x0 + (- g) < ((h + c) ^\ n) . m by XREAL_1:20;
hence y in N2 by A13, A20, A22; ::_thesis: verum
end;
then consider n being Element of NAT such that
rng (c ^\ n) c= N2 and
A23: rng ((h + c) ^\ n) c= N2 ;
consider L being LinearFunc, R being RestFunc such that
A24: for x being Real st x in N1 holds
((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5;
A25: rng (c ^\ n) c= dom (SVF1 (1,f,z0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in dom (SVF1 (1,f,z0)) )
assume A26: y in rng (c ^\ n) ; ::_thesis: y in dom (SVF1 (1,f,z0))
rng (c ^\ n) = rng c by VALUED_0:26;
then y = x0 by A10, A6, A26, TARSKI:def_1;
then y in N by A7, A14;
hence y in dom (SVF1 (1,f,z0)) by A2; ::_thesis: verum
end;
A27: L is total by FDIFF_1:def_3;
A28: ( ((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
A29: for k being Element of NAT holds s1 . k = H1(k) from SEQ_1:sch_1();
A30: 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
A31: ( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0 ) by FDIFF_1:def_2;
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 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
then consider m being Element of NAT such that
A32: for k being Element of NAT st m <= k holds
abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) < r by A31, 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 A33: 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 A29
.= abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) ;
hence abs ((s1 . k) - (L . 1)) < r by A32, A33; ::_thesis: verum
end;
consider s being Real such that
A34: for p1 being Real holds L . p1 = s * p1 by FDIFF_1:def_3;
A35: L . 1 = s * 1 by A34
.= 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
A36: (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 A34
.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)
.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A36, XCMPLX_0:def_7
.= s1 . m by A29, A35 ; ::_thesis: verum
end;
then A37: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = s1 by FUNCT_2:63;
hence ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A30, 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 A37, A30, SEQ_2:def_7; ::_thesis: verum
end;
A38: rng ((h + c) ^\ n) c= dom (SVF1 (1,f,z0))
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,z0)) )
assume y in rng ((h + c) ^\ n) ; ::_thesis: y in dom (SVF1 (1,f,z0))
then y in N2 by A23;
then y in N by A7;
hence y in dom (SVF1 (1,f,z0)) by A2; ::_thesis: verum
end;
A39: rng (h + c) c= dom (SVF1 (1,f,z0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in dom (SVF1 (1,f,z0)) )
assume y in rng (h + c) ; ::_thesis: y in dom (SVF1 (1,f,z0))
then y in N by A11;
hence y in dom (SVF1 (1,f,z0)) by A2; ::_thesis: verum
end;
A40: for k being Element of NAT holds ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,z0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))
proof
let k be Element of NAT ; ::_thesis: ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,z0)) . ((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 A41: ((h + c) ^\ n) . k in N2 by A23;
( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by VALUED_0:26, VALUED_0:28;
then A42: (c ^\ n) . k = x0 by A10, A6, TARSKI:def_1;
(((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 ;
hence ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,z0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A24, A8, A41, A42; ::_thesis: verum
end;
A43: R is total by FDIFF_1:def_2;
now__::_thesis:_for_k_being_Element_of_NAT_holds_(((SVF1_(1,f,z0))_/*_((h_+_c)_^\_n))_-_((SVF1_(1,f,z0))_/*_(c_^\_n)))_._k_=_((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_._k
let k be Element of NAT ; ::_thesis: (((SVF1 (1,f,z0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,z0)) /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k
thus (((SVF1 (1,f,z0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,z0)) /* (c ^\ n))) . k = (((SVF1 (1,f,z0)) /* ((h + c) ^\ n)) . k) - (((SVF1 (1,f,z0)) /* (c ^\ n)) . k) by RFUNCT_2:1
.= ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - (((SVF1 (1,f,z0)) /* (c ^\ n)) . k) by A38, FUNCT_2:108
.= ((SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (1,f,z0)) . ((c ^\ n) . k)) by A25, FUNCT_2:108
.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A40
.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A27, FUNCT_2:115
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A43, FUNCT_2:115
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:7 ; ::_thesis: verum
end;
then ((SVF1 (1,f,z0)) /* ((h + c) ^\ n)) - ((SVF1 (1,f,z0)) /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63;
then A44: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = ((((SVF1 (1,f,z0)) /* (h + c)) ^\ n) - ((SVF1 (1,f,z0)) /* (c ^\ n))) (#) ((h ^\ n) ") by A39, VALUED_0:27
.= ((((SVF1 (1,f,z0)) /* (h + c)) ^\ n) - (((SVF1 (1,f,z0)) /* c) ^\ n)) (#) ((h ^\ n) ") by A15, VALUED_0:27
.= ((((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) ^\ n) (#) ((h ^\ n) ") by SEQM_3:17
.= ((((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) ^\ n) (#) ((h ") ^\ n) by SEQM_3:18
.= ((((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) (#) (h ")) ^\ n by SEQM_3:19 ;
then A45: L . 1 = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) by A28, SEQ_4:22;
thus (h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)) is convergent by A28, A44, SEQ_4:21; ::_thesis: partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c)))
for x being Real st x in N2 holds
((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A24, A8;
hence partdiff (f,z0,1) = lim ((h ") (#) (((SVF1 (1,f,z0)) /* (h + c)) - ((SVF1 (1,f,z0)) /* c))) by A1, A3, A9, A45, Th11; ::_thesis: verum
end;
theorem :: PDIFF_2:18
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2
for N being Neighbourhood of (proj (2,2)) . z0 st f is_partial_differentiable_in z0,2 & N c= dom (SVF1 (2,f,z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) is convergent & partdiff (f,z0,2) = lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c))) )
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2
for N being Neighbourhood of (proj (2,2)) . z0 st f is_partial_differentiable_in z0,2 & N c= dom (SVF1 (2,f,z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) is convergent & partdiff (f,z0,2) = lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c))) )
let z0 be Element of REAL 2; ::_thesis: for N being Neighbourhood of (proj (2,2)) . z0 st f is_partial_differentiable_in z0,2 & N c= dom (SVF1 (2,f,z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) is convergent & partdiff (f,z0,2) = lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c))) )
let N be Neighbourhood of (proj (2,2)) . z0; ::_thesis: ( f is_partial_differentiable_in z0,2 & N c= dom (SVF1 (2,f,z0)) implies for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) is convergent & partdiff (f,z0,2) = lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c))) ) )
assume that
A1: f is_partial_differentiable_in z0,2 and
A2: N c= dom (SVF1 (2,f,z0)) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) is convergent & partdiff (f,z0,2) = lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c))) )
consider x0, y0 being Real such that
A3: z0 = <*x0,y0*> and
A4: ex N1 being Neighbourhood of y0 st
( N1 c= dom (SVF1 (2,f,z0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N1 holds
((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A1, Th10;
consider N1 being Neighbourhood of y0 such that
N1 c= dom (SVF1 (2,f,z0)) and
A5: ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N1 holds
((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A4;
A6: (proj (2,2)) . z0 = y0 by A3, Th2;
then consider N2 being Neighbourhood of y0 such that
A7: N2 c= N and
A8: N2 c= N1 by RCOMP_1:17;
A9: N2 c= dom (SVF1 (2,f,z0)) by A2, A7, XBOOLE_1:1;
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) is convergent & partdiff (f,z0,2) = lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c))) )
let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) is convergent & partdiff (f,z0,2) = lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c))) ) )
assume that
A10: rng c = {((proj (2,2)) . z0)} and
A11: rng (h + c) c= N ; ::_thesis: ( (h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) is convergent & partdiff (f,z0,2) = lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c))) )
consider g being real number such that
A12: 0 < g and
A13: N2 = ].(y0 - g),(y0 + g).[ by RCOMP_1:def_6;
( y0 + 0 < y0 + g & y0 - g < y0 - 0 ) by A12, XREAL_1:8, XREAL_1:44;
then A14: y0 in N2 by A13;
A15: rng c c= dom (SVF1 (2,f,z0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in dom (SVF1 (2,f,z0)) )
assume y in rng c ; ::_thesis: y in dom (SVF1 (2,f,z0))
then y = y0 by A10, A6, TARSKI:def_1;
then y in N by A7, A14;
hence y in dom (SVF1 (2,f,z0)) by A2; ::_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 A10, A6, TARSKI:def_1;
then A16: lim c = y0 by SEQ_4:25;
A17: h + c is convergent by SEQ_2:5;
lim h = 0 ;
then lim (h + c) = 0 + y0 by A16, SEQ_2:6
.= y0 ;
then consider n being Element of NAT such that
A18: for m being Element of NAT st n <= m holds
abs (((h + c) . m) - y0) < g by A12, A17, SEQ_2:def_7;
take n ; ::_thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
A19: rng (c ^\ n) = {y0} by A10, A6, VALUED_0:26;
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 A14, A19, 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
A20: y = ((h + c) ^\ n) . m by FUNCT_2:113;
n + 0 <= n + m by XREAL_1:7;
then A21: abs (((h + c) . (n + m)) - y0) < g by A18;
then ((h + c) . (m + n)) - y0 < g by SEQ_2:1;
then (((h + c) ^\ n) . m) - y0 < g by NAT_1:def_3;
then A22: ((h + c) ^\ n) . m < y0 + g by XREAL_1:19;
- g < ((h + c) . (m + n)) - y0 by A21, SEQ_2:1;
then - g < (((h + c) ^\ n) . m) - y0 by NAT_1:def_3;
then y0 + (- g) < ((h + c) ^\ n) . m by XREAL_1:20;
hence y in N2 by A13, A20, A22; ::_thesis: verum
end;
then consider n being Element of NAT such that
rng (c ^\ n) c= N2 and
A23: rng ((h + c) ^\ n) c= N2 ;
consider L being LinearFunc, R being RestFunc such that
A24: for y being Real st y in N1 holds
((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A5;
A25: rng (c ^\ n) c= dom (SVF1 (2,f,z0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in dom (SVF1 (2,f,z0)) )
assume A26: y in rng (c ^\ n) ; ::_thesis: y in dom (SVF1 (2,f,z0))
rng (c ^\ n) = rng c by VALUED_0:26;
then y = y0 by A10, A6, A26, TARSKI:def_1;
then y in N by A7, A14;
hence y in dom (SVF1 (2,f,z0)) by A2; ::_thesis: verum
end;
A27: L is total by FDIFF_1:def_3;
A28: ( ((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
A29: for k being Element of NAT holds s1 . k = H1(k) from SEQ_1:sch_1();
A30: 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
A31: ( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0 ) by FDIFF_1:def_2;
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 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
then consider m being Element of NAT such that
A32: for k being Element of NAT st m <= k holds
abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) < r by A31, 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 A33: 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 A29
.= abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0) ;
hence abs ((s1 . k) - (L . 1)) < r by A32, A33; ::_thesis: verum
end;
consider s being Real such that
A34: for p1 being Real holds L . p1 = s * p1 by FDIFF_1:def_3;
A35: L . 1 = s * 1 by A34
.= 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
A36: (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 A34
.= (s * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)
.= (s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A36, XCMPLX_0:def_7
.= s1 . m by A29, A35 ; ::_thesis: verum
end;
then A37: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = s1 by FUNCT_2:63;
hence ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A30, 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 A37, A30, SEQ_2:def_7; ::_thesis: verum
end;
A38: rng ((h + c) ^\ n) c= dom (SVF1 (2,f,z0))
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,z0)) )
assume y in rng ((h + c) ^\ n) ; ::_thesis: y in dom (SVF1 (2,f,z0))
then y in N2 by A23;
then y in N by A7;
hence y in dom (SVF1 (2,f,z0)) by A2; ::_thesis: verum
end;
A39: rng (h + c) c= dom (SVF1 (2,f,z0))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in dom (SVF1 (2,f,z0)) )
assume y in rng (h + c) ; ::_thesis: y in dom (SVF1 (2,f,z0))
then y in N by A11;
hence y in dom (SVF1 (2,f,z0)) by A2; ::_thesis: verum
end;
A40: for k being Element of NAT holds ((SVF1 (2,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (2,f,z0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))
proof
let k be Element of NAT ; ::_thesis: ((SVF1 (2,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (2,f,z0)) . ((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 A41: ((h + c) ^\ n) . k in N2 by A23;
( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by VALUED_0:26, VALUED_0:28;
then A42: (c ^\ n) . k = y0 by A10, A6, TARSKI:def_1;
(((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 ;
hence ((SVF1 (2,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (2,f,z0)) . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A24, A8, A41, A42; ::_thesis: verum
end;
A43: R is total by FDIFF_1:def_2;
now__::_thesis:_for_k_being_Element_of_NAT_holds_(((SVF1_(2,f,z0))_/*_((h_+_c)_^\_n))_-_((SVF1_(2,f,z0))_/*_(c_^\_n)))_._k_=_((L_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_._k
let k be Element of NAT ; ::_thesis: (((SVF1 (2,f,z0)) /* ((h + c) ^\ n)) - ((SVF1 (2,f,z0)) /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k
thus (((SVF1 (2,f,z0)) /* ((h + c) ^\ n)) - ((SVF1 (2,f,z0)) /* (c ^\ n))) . k = (((SVF1 (2,f,z0)) /* ((h + c) ^\ n)) . k) - (((SVF1 (2,f,z0)) /* (c ^\ n)) . k) by RFUNCT_2:1
.= ((SVF1 (2,f,z0)) . (((h + c) ^\ n) . k)) - (((SVF1 (2,f,z0)) /* (c ^\ n)) . k) by A38, FUNCT_2:108
.= ((SVF1 (2,f,z0)) . (((h + c) ^\ n) . k)) - ((SVF1 (2,f,z0)) . ((c ^\ n) . k)) by A25, FUNCT_2:108
.= (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)) by A40
.= ((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k)) by A27, FUNCT_2:115
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A43, FUNCT_2:115
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by SEQ_1:7 ; ::_thesis: verum
end;
then ((SVF1 (2,f,z0)) /* ((h + c) ^\ n)) - ((SVF1 (2,f,z0)) /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63;
then A44: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = ((((SVF1 (2,f,z0)) /* (h + c)) ^\ n) - ((SVF1 (2,f,z0)) /* (c ^\ n))) (#) ((h ^\ n) ") by A39, VALUED_0:27
.= ((((SVF1 (2,f,z0)) /* (h + c)) ^\ n) - (((SVF1 (2,f,z0)) /* c) ^\ n)) (#) ((h ^\ n) ") by A15, VALUED_0:27
.= ((((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) ^\ n) (#) ((h ^\ n) ") by SEQM_3:17
.= ((((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) ^\ n) (#) ((h ") ^\ n) by SEQM_3:18
.= ((((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) (#) (h ")) ^\ n by SEQM_3:19 ;
then A45: L . 1 = lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c))) by A28, SEQ_4:22;
thus (h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)) is convergent by A28, A44, SEQ_4:21; ::_thesis: partdiff (f,z0,2) = lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c)))
for y being Real st y in N2 holds
((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A24, A8;
hence partdiff (f,z0,2) = lim ((h ") (#) (((SVF1 (2,f,z0)) /* (h + c)) - ((SVF1 (2,f,z0)) /* c))) by A1, A3, A9, A45, Th12; ::_thesis: verum
end;
theorem :: PDIFF_2:19
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_partial_differentiable_in z0,1 & f2 is_partial_differentiable_in z0,1 holds
f1 (#) f2 is_partial_differentiable_in z0,1
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_partial_differentiable_in z0,1 & f2 is_partial_differentiable_in z0,1 holds
f1 (#) f2 is_partial_differentiable_in z0,1
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_partial_differentiable_in z0,1 & f2 is_partial_differentiable_in z0,1 implies f1 (#) f2 is_partial_differentiable_in z0,1 )
assume that
A1: f1 is_partial_differentiable_in z0,1 and
A2: f2 is_partial_differentiable_in z0,1 ; ::_thesis: f1 (#) f2 is_partial_differentiable_in z0,1
consider x0, y0 being Real such that
A3: z0 = <*x0,y0*> and
A4: ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,f1,z0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f1,z0)) . x) - ((SVF1 (1,f1,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A1, Th9;
consider N1 being Neighbourhood of x0 such that
A5: N1 c= dom (SVF1 (1,f1,z0)) and
A6: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N1 holds
((SVF1 (1,f1,z0)) . x) - ((SVF1 (1,f1,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A4;
consider L1 being LinearFunc, R1 being RestFunc such that
A7: for x being Real st x in N1 holds
((SVF1 (1,f1,z0)) . x) - ((SVF1 (1,f1,z0)) . x0) = (L1 . (x - x0)) + (R1 . (x - x0)) by A6;
consider x1, y1 being Real such that
A8: z0 = <*x1,y1*> and
A9: ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,f2,z0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,f2,z0)) . x) - ((SVF1 (1,f2,z0)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) by A2, Th9;
x0 = x1 by A3, A8, FINSEQ_1:77;
then consider N2 being Neighbourhood of x0 such that
A10: N2 c= dom (SVF1 (1,f2,z0)) and
A11: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N2 holds
((SVF1 (1,f2,z0)) . x) - ((SVF1 (1,f2,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A9;
consider L2 being LinearFunc, R2 being RestFunc such that
A12: for x being Real st x in N2 holds
((SVF1 (1,f2,z0)) . x) - ((SVF1 (1,f2,z0)) . x0) = (L2 . (x - x0)) + (R2 . (x - x0)) by A11;
consider N being Neighbourhood of x0 such that
A13: N c= N1 and
A14: N c= N2 by RCOMP_1:17;
A15: N c= dom (SVF1 (1,f2,z0)) by A10, A14, XBOOLE_1:1;
A16: N c= dom (SVF1 (1,f1,z0)) by A5, A13, XBOOLE_1:1;
A17: for y being Real st y in N holds
y in dom (SVF1 (1,(f1 (#) f2),z0))
proof
let y be Real; ::_thesis: ( y in N implies y in dom (SVF1 (1,(f1 (#) f2),z0)) )
assume A18: y in N ; ::_thesis: y in dom (SVF1 (1,(f1 (#) f2),z0))
then ( (reproj (1,z0)) . y in dom f1 & (reproj (1,z0)) . y in dom f2 ) by A16, A15, FUNCT_1:11;
then (reproj (1,z0)) . y in (dom f1) /\ (dom f2) by XBOOLE_0:def_4;
then A19: (reproj (1,z0)) . y in dom (f1 (#) f2) by VALUED_1:def_4;
y in dom (reproj (1,z0)) by A15, A18, FUNCT_1:11;
hence y in dom (SVF1 (1,(f1 (#) f2),z0)) by A19, FUNCT_1:11; ::_thesis: verum
end;
then for y being set st y in N holds
y in dom (SVF1 (1,(f1 (#) f2),z0)) ;
then A20: N c= dom (SVF1 (1,(f1 (#) f2),z0)) by TARSKI:def_3;
reconsider R12 = ((SVF1 (1,f1,z0)) . x0) (#) R2 as RestFunc by FDIFF_1:5;
A21: L2 is total by FDIFF_1:def_3;
reconsider R11 = ((SVF1 (1,f2,z0)) . x0) (#) R1 as RestFunc by FDIFF_1:5;
A22: L1 is total by FDIFF_1:def_3;
A23: R1 is total by FDIFF_1:def_2;
reconsider R17 = R1 (#) R2 as RestFunc by FDIFF_1:4;
reconsider R16 = R1 (#) L2, R18 = R2 (#) L1 as RestFunc by FDIFF_1:7;
reconsider R14 = L1 (#) L2 as RestFunc by FDIFF_1:6;
reconsider R19 = R16 + R17 as RestFunc by FDIFF_1:4;
reconsider R20 = R19 + R18 as RestFunc by FDIFF_1:4;
A24: R14 is total by FDIFF_1:def_2;
A25: R18 is total by FDIFF_1:def_2;
A26: R2 is total by FDIFF_1:def_2;
reconsider R13 = R11 + R12 as RestFunc by FDIFF_1:4;
reconsider L11 = ((SVF1 (1,f2,z0)) . x0) (#) L1, L12 = ((SVF1 (1,f1,z0)) . x0) (#) L2 as LinearFunc by FDIFF_1:3;
reconsider L = L11 + L12 as LinearFunc by FDIFF_1:2;
reconsider R15 = R13 + R14 as RestFunc by FDIFF_1:4;
reconsider R = R15 + R20 as RestFunc by FDIFF_1:4;
A27: R16 is total by FDIFF_1:def_2;
A28: ( L11 is total & L12 is total ) by FDIFF_1:def_3;
now__::_thesis:_for_x_being_Real_st_x_in_N_holds_
((SVF1_(1,(f1_(#)_f2),z0))_._x)_-_((SVF1_(1,(f1_(#)_f2),z0))_._x0)_=_(L_._(x_-_x0))_+_(R_._(x_-_x0))
A29: x0 in dom ((f1 (#) f2) * (reproj (1,z0))) by A17, RCOMP_1:16;
then A30: x0 in dom (reproj (1,z0)) by FUNCT_1:11;
(reproj (1,z0)) . x0 in dom (f1 (#) f2) by A29, FUNCT_1:11;
then A31: (reproj (1,z0)) . x0 in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then (reproj (1,z0)) . x0 in dom f1 by XBOOLE_0:def_4;
then A32: x0 in dom (f1 * (reproj (1,z0))) by A30, FUNCT_1:11;
(reproj (1,z0)) . x0 in dom f2 by A31, XBOOLE_0:def_4;
then A33: x0 in dom (f2 * (reproj (1,z0))) by A30, FUNCT_1:11;
let x be Real; ::_thesis: ( x in N implies ((SVF1 (1,(f1 (#) f2),z0)) . x) - ((SVF1 (1,(f1 (#) f2),z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
A34: x0 in N by RCOMP_1:16;
assume A35: x in N ; ::_thesis: ((SVF1 (1,(f1 (#) f2),z0)) . x) - ((SVF1 (1,(f1 (#) f2),z0)) . x0) = (L . (x - x0)) + (R . (x - x0))
then A36: (((SVF1 (1,f1,z0)) . x) - ((SVF1 (1,f1,z0)) . x0)) + ((SVF1 (1,f1,z0)) . x0) = ((L1 . (x - x0)) + (R1 . (x - x0))) + ((SVF1 (1,f1,z0)) . x0) by A7, A13;
A37: x in dom ((f1 (#) f2) * (reproj (1,z0))) by A17, A35;
then A38: x in dom (reproj (1,z0)) by FUNCT_1:11;
(reproj (1,z0)) . x in dom (f1 (#) f2) by A37, FUNCT_1:11;
then A39: (reproj (1,z0)) . x in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then (reproj (1,z0)) . x in dom f1 by XBOOLE_0:def_4;
then A40: x in dom (f1 * (reproj (1,z0))) by A38, FUNCT_1:11;
(reproj (1,z0)) . x in dom f2 by A39, XBOOLE_0:def_4;
then A41: x in dom (f2 * (reproj (1,z0))) by A38, FUNCT_1:11;
thus ((SVF1 (1,(f1 (#) f2),z0)) . x) - ((SVF1 (1,(f1 (#) f2),z0)) . x0) = ((f1 (#) f2) . ((reproj (1,z0)) . x)) - ((SVF1 (1,(f1 (#) f2),z0)) . x0) by A20, A35, FUNCT_1:12
.= ((f1 . ((reproj (1,z0)) . x)) * (f2 . ((reproj (1,z0)) . x))) - ((SVF1 (1,(f1 (#) f2),z0)) . x0) by VALUED_1:5
.= (((SVF1 (1,f1,z0)) . x) * (f2 . ((reproj (1,z0)) . x))) - ((SVF1 (1,(f1 (#) f2),z0)) . x0) by A40, FUNCT_1:12
.= (((SVF1 (1,f1,z0)) . x) * ((SVF1 (1,f2,z0)) . x)) - (((f1 (#) f2) * (reproj (1,z0))) . x0) by A41, FUNCT_1:12
.= (((SVF1 (1,f1,z0)) . x) * ((SVF1 (1,f2,z0)) . x)) - ((f1 (#) f2) . ((reproj (1,z0)) . x0)) by A20, A34, FUNCT_1:12
.= (((SVF1 (1,f1,z0)) . x) * ((SVF1 (1,f2,z0)) . x)) - ((f1 . ((reproj (1,z0)) . x0)) * (f2 . ((reproj (1,z0)) . x0))) by VALUED_1:5
.= (((SVF1 (1,f1,z0)) . x) * ((SVF1 (1,f2,z0)) . x)) - (((SVF1 (1,f1,z0)) . x0) * (f2 . ((reproj (1,z0)) . x0))) by A32, FUNCT_1:12
.= (((((SVF1 (1,f1,z0)) . x) * ((SVF1 (1,f2,z0)) . x)) + (- (((SVF1 (1,f1,z0)) . x) * ((SVF1 (1,f2,z0)) . x0)))) + (((SVF1 (1,f1,z0)) . x) * ((SVF1 (1,f2,z0)) . x0))) - (((SVF1 (1,f1,z0)) . x0) * ((SVF1 (1,f2,z0)) . x0)) by A33, FUNCT_1:12
.= (((SVF1 (1,f1,z0)) . x) * (((SVF1 (1,f2,z0)) . x) - ((SVF1 (1,f2,z0)) . x0))) + ((((SVF1 (1,f1,z0)) . x) - ((SVF1 (1,f1,z0)) . x0)) * ((SVF1 (1,f2,z0)) . x0))
.= (((SVF1 (1,f1,z0)) . x) * (((SVF1 (1,f2,z0)) . x) - ((SVF1 (1,f2,z0)) . x0))) + (((L1 . (x - x0)) + (R1 . (x - x0))) * ((SVF1 (1,f2,z0)) . x0)) by A7, A13, A35
.= (((SVF1 (1,f1,z0)) . x) * (((SVF1 (1,f2,z0)) . x) - ((SVF1 (1,f2,z0)) . x0))) + ((((SVF1 (1,f2,z0)) . x0) * (L1 . (x - x0))) + (((SVF1 (1,f2,z0)) . x0) * (R1 . (x - x0))))
.= (((SVF1 (1,f1,z0)) . x) * (((SVF1 (1,f2,z0)) . x) - ((SVF1 (1,f2,z0)) . x0))) + ((L11 . (x - x0)) + (((SVF1 (1,f2,z0)) . x0) * (R1 . (x - x0)))) by A22, RFUNCT_1:57
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) + ((SVF1 (1,f1,z0)) . x0)) * (((SVF1 (1,f2,z0)) . x) - ((SVF1 (1,f2,z0)) . x0))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A23, A36, RFUNCT_1:57
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) + ((SVF1 (1,f1,z0)) . x0)) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A12, A14, A35
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((((SVF1 (1,f1,z0)) . x0) * (L2 . (x - x0))) + (((SVF1 (1,f1,z0)) . 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,z0)) . x0) * (R2 . (x - x0))))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A21, 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 A26, 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 A23, A26, 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 A28, 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 A22, A21, 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 A22, A26, 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 A21, A23, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + (R17 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0))) by A23, A26, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + (R19 . (x - x0))) + ((L . (x - x0)) + (R13 . (x - x0))) by A23, A26, A27, 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 A23, A26, A27, A25, 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 A23, A26, A24, RFUNCT_1:56
.= (L . (x - x0)) + (R . (x - x0)) by A23, A26, A24, A27, A25, RFUNCT_1:56 ; ::_thesis: verum
end;
hence f1 (#) f2 is_partial_differentiable_in z0,1 by A3, A20, Th9; ::_thesis: verum
end;
theorem :: PDIFF_2:20
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_partial_differentiable_in z0,2 & f2 is_partial_differentiable_in z0,2 holds
f1 (#) f2 is_partial_differentiable_in z0,2
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_partial_differentiable_in z0,2 & f2 is_partial_differentiable_in z0,2 holds
f1 (#) f2 is_partial_differentiable_in z0,2
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_partial_differentiable_in z0,2 & f2 is_partial_differentiable_in z0,2 implies f1 (#) f2 is_partial_differentiable_in z0,2 )
assume that
A1: f1 is_partial_differentiable_in z0,2 and
A2: f2 is_partial_differentiable_in z0,2 ; ::_thesis: f1 (#) f2 is_partial_differentiable_in z0,2
consider x0, y0 being Real such that
A3: z0 = <*x0,y0*> and
A4: ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f1,z0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f1,z0)) . y) - ((SVF1 (2,f1,z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A1, Th10;
consider N1 being Neighbourhood of y0 such that
A5: N1 c= dom (SVF1 (2,f1,z0)) and
A6: ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N1 holds
((SVF1 (2,f1,z0)) . y) - ((SVF1 (2,f1,z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A4;
consider L1 being LinearFunc, R1 being RestFunc such that
A7: for y being Real st y in N1 holds
((SVF1 (2,f1,z0)) . y) - ((SVF1 (2,f1,z0)) . y0) = (L1 . (y - y0)) + (R1 . (y - y0)) by A6;
consider x1, y1 being Real such that
A8: z0 = <*x1,y1*> and
A9: ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,f2,z0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f2,z0)) . y) - ((SVF1 (2,f2,z0)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) by A2, Th10;
y0 = y1 by A3, A8, FINSEQ_1:77;
then consider N2 being Neighbourhood of y0 such that
A10: N2 c= dom (SVF1 (2,f2,z0)) and
A11: ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N2 holds
((SVF1 (2,f2,z0)) . y) - ((SVF1 (2,f2,z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A9;
consider L2 being LinearFunc, R2 being RestFunc such that
A12: for y being Real st y in N2 holds
((SVF1 (2,f2,z0)) . y) - ((SVF1 (2,f2,z0)) . y0) = (L2 . (y - y0)) + (R2 . (y - y0)) by A11;
consider N being Neighbourhood of y0 such that
A13: N c= N1 and
A14: N c= N2 by RCOMP_1:17;
A15: N c= dom (SVF1 (2,f2,z0)) by A10, A14, XBOOLE_1:1;
A16: N c= dom (SVF1 (2,f1,z0)) by A5, A13, XBOOLE_1:1;
A17: for y being Real st y in N holds
y in dom (SVF1 (2,(f1 (#) f2),z0))
proof
let y be Real; ::_thesis: ( y in N implies y in dom (SVF1 (2,(f1 (#) f2),z0)) )
assume A18: y in N ; ::_thesis: y in dom (SVF1 (2,(f1 (#) f2),z0))
then ( (reproj (2,z0)) . y in dom f1 & (reproj (2,z0)) . y in dom f2 ) by A16, A15, FUNCT_1:11;
then (reproj (2,z0)) . y in (dom f1) /\ (dom f2) by XBOOLE_0:def_4;
then A19: (reproj (2,z0)) . y in dom (f1 (#) f2) by VALUED_1:def_4;
y in dom (reproj (2,z0)) by A15, A18, FUNCT_1:11;
hence y in dom (SVF1 (2,(f1 (#) f2),z0)) by A19, FUNCT_1:11; ::_thesis: verum
end;
then for y being set st y in N holds
y in dom (SVF1 (2,(f1 (#) f2),z0)) ;
then A20: N c= dom (SVF1 (2,(f1 (#) f2),z0)) by TARSKI:def_3;
reconsider L12 = ((SVF1 (2,f1,z0)) . y0) (#) L2 as LinearFunc by FDIFF_1:3;
A21: L2 is total by FDIFF_1:def_3;
reconsider L11 = ((SVF1 (2,f2,z0)) . y0) (#) L1 as LinearFunc by FDIFF_1:3;
A22: L1 is total by FDIFF_1:def_3;
reconsider L = L11 + L12 as LinearFunc by FDIFF_1:2;
A23: R1 is total by FDIFF_1:def_2;
reconsider R16 = R1 (#) L2, R18 = R2 (#) L1 as RestFunc by FDIFF_1:7;
reconsider R14 = L1 (#) L2 as RestFunc by FDIFF_1:6;
reconsider R11 = ((SVF1 (2,f2,z0)) . y0) (#) R1, R12 = ((SVF1 (2,f1,z0)) . y0) (#) R2 as RestFunc by FDIFF_1:5;
reconsider R13 = R11 + R12 as RestFunc by FDIFF_1:4;
reconsider R15 = R13 + R14, 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;
A24: R14 is total by FDIFF_1:def_2;
A25: R16 is total by FDIFF_1:def_2;
A26: R18 is total by FDIFF_1:def_2;
A27: R2 is total by FDIFF_1:def_2;
A28: ( L11 is total & L12 is total ) by FDIFF_1:def_3;
now__::_thesis:_for_y_being_Real_st_y_in_N_holds_
((SVF1_(2,(f1_(#)_f2),z0))_._y)_-_((SVF1_(2,(f1_(#)_f2),z0))_._y0)_=_(L_._(y_-_y0))_+_(R_._(y_-_y0))
A29: y0 in dom ((f1 (#) f2) * (reproj (2,z0))) by A17, RCOMP_1:16;
then A30: y0 in dom (reproj (2,z0)) by FUNCT_1:11;
(reproj (2,z0)) . y0 in dom (f1 (#) f2) by A29, FUNCT_1:11;
then A31: (reproj (2,z0)) . y0 in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then (reproj (2,z0)) . y0 in dom f1 by XBOOLE_0:def_4;
then A32: y0 in dom (f1 * (reproj (2,z0))) by A30, FUNCT_1:11;
(reproj (2,z0)) . y0 in dom f2 by A31, XBOOLE_0:def_4;
then A33: y0 in dom (f2 * (reproj (2,z0))) by A30, FUNCT_1:11;
let y be Real; ::_thesis: ( y in N implies ((SVF1 (2,(f1 (#) f2),z0)) . y) - ((SVF1 (2,(f1 (#) f2),z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
A34: y0 in N by RCOMP_1:16;
assume A35: y in N ; ::_thesis: ((SVF1 (2,(f1 (#) f2),z0)) . y) - ((SVF1 (2,(f1 (#) f2),z0)) . y0) = (L . (y - y0)) + (R . (y - y0))
then A36: (((SVF1 (2,f1,z0)) . y) - ((SVF1 (2,f1,z0)) . y0)) + ((SVF1 (2,f1,z0)) . y0) = ((L1 . (y - y0)) + (R1 . (y - y0))) + ((SVF1 (2,f1,z0)) . y0) by A7, A13;
A37: y in dom ((f1 (#) f2) * (reproj (2,z0))) by A17, A35;
then A38: y in dom (reproj (2,z0)) by FUNCT_1:11;
(reproj (2,z0)) . y in dom (f1 (#) f2) by A37, FUNCT_1:11;
then A39: (reproj (2,z0)) . y in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then (reproj (2,z0)) . y in dom f1 by XBOOLE_0:def_4;
then A40: y in dom (f1 * (reproj (2,z0))) by A38, FUNCT_1:11;
(reproj (2,z0)) . y in dom f2 by A39, XBOOLE_0:def_4;
then A41: y in dom (f2 * (reproj (2,z0))) by A38, FUNCT_1:11;
thus ((SVF1 (2,(f1 (#) f2),z0)) . y) - ((SVF1 (2,(f1 (#) f2),z0)) . y0) = ((f1 (#) f2) . ((reproj (2,z0)) . y)) - ((SVF1 (2,(f1 (#) f2),z0)) . y0) by A20, A35, FUNCT_1:12
.= ((f1 . ((reproj (2,z0)) . y)) * (f2 . ((reproj (2,z0)) . y))) - ((SVF1 (2,(f1 (#) f2),z0)) . y0) by VALUED_1:5
.= (((SVF1 (2,f1,z0)) . y) * (f2 . ((reproj (2,z0)) . y))) - ((SVF1 (2,(f1 (#) f2),z0)) . y0) by A40, FUNCT_1:12
.= (((SVF1 (2,f1,z0)) . y) * ((SVF1 (2,f2,z0)) . y)) - (((f1 (#) f2) * (reproj (2,z0))) . y0) by A41, FUNCT_1:12
.= (((SVF1 (2,f1,z0)) . y) * ((SVF1 (2,f2,z0)) . y)) - ((f1 (#) f2) . ((reproj (2,z0)) . y0)) by A20, A34, FUNCT_1:12
.= (((SVF1 (2,f1,z0)) . y) * ((SVF1 (2,f2,z0)) . y)) - ((f1 . ((reproj (2,z0)) . y0)) * (f2 . ((reproj (2,z0)) . y0))) by VALUED_1:5
.= (((SVF1 (2,f1,z0)) . y) * ((SVF1 (2,f2,z0)) . y)) - (((SVF1 (2,f1,z0)) . y0) * (f2 . ((reproj (2,z0)) . y0))) by A32, FUNCT_1:12
.= (((((SVF1 (2,f1,z0)) . y) * ((SVF1 (2,f2,z0)) . y)) + (- (((SVF1 (2,f1,z0)) . y) * ((SVF1 (2,f2,z0)) . y0)))) + (((SVF1 (2,f1,z0)) . y) * ((SVF1 (2,f2,z0)) . y0))) - (((SVF1 (2,f1,z0)) . y0) * ((SVF1 (2,f2,z0)) . y0)) by A33, FUNCT_1:12
.= (((SVF1 (2,f1,z0)) . y) * (((SVF1 (2,f2,z0)) . y) - ((SVF1 (2,f2,z0)) . y0))) + ((((SVF1 (2,f1,z0)) . y) - ((SVF1 (2,f1,z0)) . y0)) * ((SVF1 (2,f2,z0)) . y0))
.= (((SVF1 (2,f1,z0)) . y) * (((SVF1 (2,f2,z0)) . y) - ((SVF1 (2,f2,z0)) . y0))) + (((L1 . (y - y0)) + (R1 . (y - y0))) * ((SVF1 (2,f2,z0)) . y0)) by A7, A13, A35
.= (((SVF1 (2,f1,z0)) . y) * (((SVF1 (2,f2,z0)) . y) - ((SVF1 (2,f2,z0)) . y0))) + ((((SVF1 (2,f2,z0)) . y0) * (L1 . (y - y0))) + (((SVF1 (2,f2,z0)) . y0) * (R1 . (y - y0))))
.= (((SVF1 (2,f1,z0)) . y) * (((SVF1 (2,f2,z0)) . y) - ((SVF1 (2,f2,z0)) . y0))) + ((L11 . (y - y0)) + (((SVF1 (2,f2,z0)) . y0) * (R1 . (y - y0)))) by A22, RFUNCT_1:57
.= ((((L1 . (y - y0)) + (R1 . (y - y0))) + ((SVF1 (2,f1,z0)) . y0)) * (((SVF1 (2,f2,z0)) . y) - ((SVF1 (2,f2,z0)) . y0))) + ((L11 . (y - y0)) + (R11 . (y - y0))) by A23, A36, RFUNCT_1:57
.= ((((L1 . (y - y0)) + (R1 . (y - y0))) + ((SVF1 (2,f1,z0)) . y0)) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L11 . (y - y0)) + (R11 . (y - y0))) by A12, A14, A35
.= ((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((((SVF1 (2,f1,z0)) . y0) * (L2 . (y - y0))) + (((SVF1 (2,f1,z0)) . 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,z0)) . y0) * (R2 . (y - y0))))) + ((L11 . (y - y0)) + (R11 . (y - y0))) by A21, 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 A27, 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 A23, A27, 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 A28, 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 A22, A21, 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 A22, A27, 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 A21, A23, RFUNCT_1:56
.= (((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + (R17 . (y - y0)))) + ((L . (y - y0)) + (R13 . (y - y0))) by A23, A27, RFUNCT_1:56
.= (((R14 . (y - y0)) + (R18 . (y - y0))) + (R19 . (y - y0))) + ((L . (y - y0)) + (R13 . (y - y0))) by A23, A27, A25, 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 A23, A27, A25, A26, 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 A23, A27, A24, RFUNCT_1:56
.= (L . (y - y0)) + (R . (y - y0)) by A23, A27, A24, A25, A26, RFUNCT_1:56 ; ::_thesis: verum
end;
hence f1 (#) f2 is_partial_differentiable_in z0,2 by A3, A20, Th10; ::_thesis: verum
end;
theorem :: PDIFF_2:21
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2 st f is_partial_differentiable_in z0,1 holds
SVF1 (1,f,z0) is_continuous_in (proj (1,2)) . z0
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 st f is_partial_differentiable_in z0,1 holds
SVF1 (1,f,z0) is_continuous_in (proj (1,2)) . z0
let z0 be Element of REAL 2; ::_thesis: ( f is_partial_differentiable_in z0,1 implies SVF1 (1,f,z0) is_continuous_in (proj (1,2)) . z0 )
assume f is_partial_differentiable_in z0,1 ; ::_thesis: SVF1 (1,f,z0) is_continuous_in (proj (1,2)) . z0
then consider x0, y0 being Real such that
A1: z0 = <*x0,y0*> and
A2: SVF1 (1,f,z0) is_differentiable_in x0 by Th5;
SVF1 (1,f,z0) is_continuous_in x0 by A2, FDIFF_1:24;
hence SVF1 (1,f,z0) is_continuous_in (proj (1,2)) . z0 by A1, Th1; ::_thesis: verum
end;
theorem :: PDIFF_2:22
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2 st f is_partial_differentiable_in z0,2 holds
SVF1 (2,f,z0) is_continuous_in (proj (2,2)) . z0
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 st f is_partial_differentiable_in z0,2 holds
SVF1 (2,f,z0) is_continuous_in (proj (2,2)) . z0
let z0 be Element of REAL 2; ::_thesis: ( f is_partial_differentiable_in z0,2 implies SVF1 (2,f,z0) is_continuous_in (proj (2,2)) . z0 )
assume f is_partial_differentiable_in z0,2 ; ::_thesis: SVF1 (2,f,z0) is_continuous_in (proj (2,2)) . z0
then consider x0, y0 being Real such that
A1: z0 = <*x0,y0*> and
A2: SVF1 (2,f,z0) is_differentiable_in y0 by Th6;
SVF1 (2,f,z0) is_continuous_in y0 by A2, FDIFF_1:24;
hence SVF1 (2,f,z0) is_continuous_in (proj (2,2)) . z0 by A1, Th2; ::_thesis: verum
end;