:: 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;