:: by Noboru Endou , Yasunari Shidama and Keiichi Miyajima

::

:: Received June 6, 2007

:: Copyright (c) 2007-2021 Association of Mizar Users

definition

let i, n be Nat;

ex b_{1} being Function of (REAL n),REAL st

for x being Element of REAL n holds b_{1} . x = x . i

for b_{1}, b_{2} being Function of (REAL n),REAL st ( for x being Element of REAL n holds b_{1} . x = x . i ) & ( for x being Element of REAL n holds b_{2} . x = x . i ) holds

b_{1} = b_{2}

end;
func proj (i,n) -> Function of (REAL n),REAL means :Def1: :: PDIFF_1:def 1

for x being Element of REAL n holds it . x = x . i;

existence for x being Element of REAL n holds it . x = x . i;

ex b

for x being Element of REAL n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines proj PDIFF_1:def 1 :

for i, n being Nat

for b_{3} being Function of (REAL n),REAL holds

( b_{3} = proj (i,n) iff for x being Element of REAL n holds b_{3} . x = x . i );

for i, n being Nat

for b

( b

set W = (proj (1,1)) " ;

Lm1: ( proj (1,1) is bijective & dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Real holds

( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )

proof end;

Lm2: for i, n being Nat st i in Seg n holds

proj (i,n) is onto

proof end;

theorem :: PDIFF_1:1

( ( for i, n being Nat st i in Seg n holds

( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL ) ) & ( for x being Real holds

( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )

( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL ) ) & ( for x being Real holds

( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )

proof end;

theorem Th2: :: PDIFF_1:2

( (proj (1,1)) " is Function of REAL,(REAL 1) & (proj (1,1)) " is one-to-one & dom ((proj (1,1)) ") = REAL & rng ((proj (1,1)) ") = REAL 1 & ex g being Function of REAL,(REAL 1) st

( g is bijective & (proj (1,1)) " = g ) )

( g is bijective & (proj (1,1)) " = g ) )

proof end;

definition

let g be PartFunc of REAL,REAL;

(((proj (1,1)) ") * g) * (proj (1,1)) is PartFunc of (REAL 1),(REAL 1)

end;
func <>* g -> PartFunc of (REAL 1),(REAL 1) equals :: PDIFF_1:def 2

(((proj (1,1)) ") * g) * (proj (1,1));

coherence (((proj (1,1)) ") * g) * (proj (1,1));

(((proj (1,1)) ") * g) * (proj (1,1)) is PartFunc of (REAL 1),(REAL 1)

proof end;

:: deftheorem defines <>* PDIFF_1:def 2 :

for g being PartFunc of REAL,REAL holds <>* g = (((proj (1,1)) ") * g) * (proj (1,1));

for g being PartFunc of REAL,REAL holds <>* g = (((proj (1,1)) ") * g) * (proj (1,1));

definition

let n be Nat;

let g be PartFunc of (REAL n),REAL;

correctness

coherence

((proj (1,1)) ") * g is PartFunc of (REAL n),(REAL 1);

end;
let g be PartFunc of (REAL n),REAL;

correctness

coherence

((proj (1,1)) ") * g is PartFunc of (REAL n),(REAL 1);

proof end;

:: deftheorem defines <>* PDIFF_1:def 3 :

for n being Nat

for g being PartFunc of (REAL n),REAL holds <>* g = ((proj (1,1)) ") * g;

for n being Nat

for g being PartFunc of (REAL n),REAL holds <>* g = ((proj (1,1)) ") * g;

definition

let i, n be Nat;

ex b_{1} being Function of (REAL-NS n),(REAL-NS 1) st

for x being Point of (REAL-NS n) holds b_{1} . x = <*((proj (i,n)) . x)*>

for b_{1}, b_{2} being Function of (REAL-NS n),(REAL-NS 1) st ( for x being Point of (REAL-NS n) holds b_{1} . x = <*((proj (i,n)) . x)*> ) & ( for x being Point of (REAL-NS n) holds b_{2} . x = <*((proj (i,n)) . x)*> ) holds

b_{1} = b_{2}

end;
func Proj (i,n) -> Function of (REAL-NS n),(REAL-NS 1) means :Def4: :: PDIFF_1:def 4

for x being Point of (REAL-NS n) holds it . x = <*((proj (i,n)) . x)*>;

existence for x being Point of (REAL-NS n) holds it . x = <*((proj (i,n)) . x)*>;

ex b

for x being Point of (REAL-NS n) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines Proj PDIFF_1:def 4 :

for i, n being Nat

for b_{3} being Function of (REAL-NS n),(REAL-NS 1) holds

( b_{3} = Proj (i,n) iff for x being Point of (REAL-NS n) holds b_{3} . x = <*((proj (i,n)) . x)*> );

for i, n being Nat

for b

( b

definition

let i be Nat;

let x be FinSequence of REAL ;

ex b_{1} being Function st

( dom b_{1} = REAL & ( for r being Element of REAL holds b_{1} . r = Replace (x,i,r) ) )

for b_{1}, b_{2} being Function st dom b_{1} = REAL & ( for r being Element of REAL holds b_{1} . r = Replace (x,i,r) ) & dom b_{2} = REAL & ( for r being Element of REAL holds b_{2} . r = Replace (x,i,r) ) holds

b_{1} = b_{2}

end;
let x be FinSequence of REAL ;

func reproj (i,x) -> Function means :Def5: :: PDIFF_1:def 5

( dom it = REAL & ( for r being Element of REAL holds it . r = Replace (x,i,r) ) );

existence ( dom it = REAL & ( for r being Element of REAL holds it . r = Replace (x,i,r) ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines reproj PDIFF_1:def 5 :

for i being Nat

for x being FinSequence of REAL

for b_{3} being Function holds

( b_{3} = reproj (i,x) iff ( dom b_{3} = REAL & ( for r being Element of REAL holds b_{3} . r = Replace (x,i,r) ) ) );

for i being Nat

for x being FinSequence of REAL

for b

( b

definition

let n, i be Nat;

let x be Element of REAL n;

:: original: reproj

redefine func reproj (i,x) -> Function of REAL,(REAL n);

correctness

coherence

reproj (i,x) is Function of REAL,(REAL n);

end;
let x be Element of REAL n;

:: original: reproj

redefine func reproj (i,x) -> Function of REAL,(REAL n);

correctness

coherence

reproj (i,x) is Function of REAL,(REAL n);

proof end;

definition

let n, i be Nat;

let x be Point of (REAL-NS n);

ex b_{1} being Function of (REAL-NS 1),(REAL-NS n) st

for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & b_{1} . r = (reproj (i,y)) . q )

for b_{1}, b_{2} being Function of (REAL-NS 1),(REAL-NS n) st ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & b_{1} . r = (reproj (i,y)) . q ) ) & ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & b_{2} . r = (reproj (i,y)) . q ) ) holds

b_{1} = b_{2}

end;
let x be Point of (REAL-NS n);

func reproj (i,x) -> Function of (REAL-NS 1),(REAL-NS n) means :Def6: :: PDIFF_1:def 6

for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & it . r = (reproj (i,y)) . q );

existence for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & it . r = (reproj (i,y)) . q );

ex b

for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & b

proof end;

uniqueness for b

( r = <*q*> & y = x & b

( r = <*q*> & y = x & b

b

proof end;

:: deftheorem Def6 defines reproj PDIFF_1:def 6 :

for n, i being Nat

for x being Point of (REAL-NS n)

for b_{4} being Function of (REAL-NS 1),(REAL-NS n) holds

( b_{4} = reproj (i,x) iff for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & b_{4} . r = (reproj (i,y)) . q ) );

for n, i being Nat

for x being Point of (REAL-NS n)

for b

( b

( r = <*q*> & y = x & b

definition

let m, n be non zero Nat;

let f be PartFunc of (REAL m),(REAL n);

let x be Element of REAL m;

end;
let f be PartFunc of (REAL m),(REAL n);

let x be Element of REAL m;

pred f is_differentiable_in x means :: PDIFF_1:def 7

ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & g is_differentiable_in y );

ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & g is_differentiable_in y );

:: deftheorem defines is_differentiable_in PDIFF_1:def 7 :

for m, n being non zero Nat

for f being PartFunc of (REAL m),(REAL n)

for x being Element of REAL m holds

( f is_differentiable_in x iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & g is_differentiable_in y ) );

for m, n being non zero Nat

for f being PartFunc of (REAL m),(REAL n)

for x being Element of REAL m holds

( f is_differentiable_in x iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & g is_differentiable_in y ) );

definition

let m, n be non zero Nat;

let f be PartFunc of (REAL m),(REAL n);

let x be Element of REAL m;

assume A1: f is_differentiable_in x ;

existence

ex b_{1} being Function of (REAL m),(REAL n) ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & b_{1} = diff (g,y) );

uniqueness

for b_{1}, b_{2} being Function of (REAL m),(REAL n) st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & b_{1} = diff (g,y) ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & b_{2} = diff (g,y) ) holds

b_{1} = b_{2};

end;
let f be PartFunc of (REAL m),(REAL n);

let x be Element of REAL m;

assume A1: f is_differentiable_in x ;

func diff (f,x) -> Function of (REAL m),(REAL n) means :Def8: :: PDIFF_1:def 8

ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & it = diff (g,y) );

correctness ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & it = diff (g,y) );

existence

ex b

( f = g & x = y & b

uniqueness

for b

( f = g & x = y & b

( f = g & x = y & b

b

proof end;

:: deftheorem Def8 defines diff PDIFF_1:def 8 :

for m, n being non zero Nat

for f being PartFunc of (REAL m),(REAL n)

for x being Element of REAL m st f is_differentiable_in x holds

for b_{5} being Function of (REAL m),(REAL n) holds

( b_{5} = diff (f,x) iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & b_{5} = diff (g,y) ) );

for m, n being non zero Nat

for f being PartFunc of (REAL m),(REAL n)

for x being Element of REAL m st f is_differentiable_in x holds

for b

( b

( f = g & x = y & b

theorem Th3: :: PDIFF_1:3

for I being Function of REAL,(REAL 1) st I = (proj (1,1)) " holds

( ( for x being VECTOR of (REAL-NS 1)

for y being Real st x = I . y holds

||.x.|| = |.y.| ) & ( for x, y being VECTOR of (REAL-NS 1)

for a, b being Real st x = I . a & y = I . b holds

x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1)

for y, a being Real st x = I . y holds

a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)

for a being Real st x = I . a holds

- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)

for a, b being Real st x = I . a & y = I . b holds

x - y = I . (a - b) ) )

( ( for x being VECTOR of (REAL-NS 1)

for y being Real st x = I . y holds

||.x.|| = |.y.| ) & ( for x, y being VECTOR of (REAL-NS 1)

for a, b being Real st x = I . a & y = I . b holds

x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1)

for y, a being Real st x = I . y holds

a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1)

for a being Real st x = I . a holds

- x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1)

for a, b being Real st x = I . a & y = I . b holds

x - y = I . (a - b) ) )

proof end;

reconsider I = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2;

theorem Th4: :: PDIFF_1:4

for J being Function of (REAL 1),REAL st J = proj (1,1) holds

( ( for x being VECTOR of (REAL-NS 1)

for y being Real st J . x = y holds

||.x.|| = |.y.| ) & ( for x, y being VECTOR of (REAL-NS 1)

for a, b being Real st J . x = a & J . y = b holds

J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)

for y, a being Real st J . x = y holds

J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)

for a being Real st J . x = a holds

J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)

for a, b being Real st J . x = a & J . y = b holds

J . (x - y) = a - b ) )

( ( for x being VECTOR of (REAL-NS 1)

for y being Real st J . x = y holds

||.x.|| = |.y.| ) & ( for x, y being VECTOR of (REAL-NS 1)

for a, b being Real st J . x = a & J . y = b holds

J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1)

for y, a being Real st J . x = y holds

J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1)

for a being Real st J . x = a holds

J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1)

for a, b being Real st J . x = a & J . y = b holds

J . (x - y) = a - b ) )

proof end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem Th5: :: PDIFF_1:5

for I being Function of REAL,(REAL 1)

for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds

( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )

for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds

( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )

proof end;

theorem Th6: :: PDIFF_1:6

for I being Function of REAL,(REAL 1)

for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds

( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) )

for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds

( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) )

proof end;

theorem Th7: :: PDIFF_1:7

for f being PartFunc of (REAL-NS 1),(REAL-NS 1)

for g being PartFunc of REAL,REAL

for x being Point of (REAL-NS 1)

for y being Real st f = <>* g & x = <*y*> & f is_differentiable_in x holds

( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 )

for g being PartFunc of REAL,REAL

for x being Point of (REAL-NS 1)

for y being Real st f = <>* g & x = <*y*> & f is_differentiable_in x holds

( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 )

proof end;

theorem Th8: :: PDIFF_1:8

for f being PartFunc of (REAL-NS 1),(REAL-NS 1)

for g being PartFunc of REAL,REAL

for x being Point of (REAL-NS 1)

for y being Real st f = <>* g & x = <*y*> & g is_differentiable_in y holds

( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )

for g being PartFunc of REAL,REAL

for x being Point of (REAL-NS 1)

for y being Real st f = <>* g & x = <*y*> & g is_differentiable_in y holds

( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )

proof end;

theorem :: PDIFF_1:9

theorem Th10: :: PDIFF_1:10

for f being PartFunc of (REAL-NS 1),(REAL-NS 1)

for g being PartFunc of REAL,REAL

for x being Point of (REAL-NS 1)

for y being Real st f = <>* g & x = <*y*> & f is_differentiable_in x holds

(diff (f,x)) . <*1*> = <*(diff (g,y))*>

for g being PartFunc of REAL,REAL

for x being Point of (REAL-NS 1)

for y being Real st f = <>* g & x = <*y*> & f is_differentiable_in x holds

(diff (f,x)) . <*1*> = <*(diff (g,y))*>

proof end;

definition

let n, m be non zero Nat;

let i be Nat;

let f be PartFunc of (REAL-NS m),(REAL-NS n);

let x be Point of (REAL-NS m);

end;
let i be Nat;

let f be PartFunc of (REAL-NS m),(REAL-NS n);

let x be Point of (REAL-NS m);

pred f is_partial_differentiable_in x,i means :: PDIFF_1:def 9

f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x;

f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x;

:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 9 :

for n, m being non zero Nat

for i being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) holds

( f is_partial_differentiable_in x,i iff f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x );

for n, m being non zero Nat

for i being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) holds

( f is_partial_differentiable_in x,i iff f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x );

definition

let m, n be non zero Nat;

let i be Nat;

let f be PartFunc of (REAL-NS m),(REAL-NS n);

let x be Point of (REAL-NS m);

diff ((f * (reproj (i,x))),((Proj (i,m)) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) ;

end;
let i be Nat;

let f be PartFunc of (REAL-NS m),(REAL-NS n);

let x be Point of (REAL-NS m);

func partdiff (f,x,i) -> Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) equals :: PDIFF_1:def 10

diff ((f * (reproj (i,x))),((Proj (i,m)) . x));

coherence diff ((f * (reproj (i,x))),((Proj (i,m)) . x));

diff ((f * (reproj (i,x))),((Proj (i,m)) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) ;

:: deftheorem defines partdiff PDIFF_1:def 10 :

for m, n being non zero Nat

for i being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) holds partdiff (f,x,i) = diff ((f * (reproj (i,x))),((Proj (i,m)) . x));

for m, n being non zero Nat

for i being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) holds partdiff (f,x,i) = diff ((f * (reproj (i,x))),((Proj (i,m)) . x));

definition

let n be non zero Nat;

let i be Nat;

let f be PartFunc of (REAL n),REAL;

let x be Element of REAL n;

end;
let i be Nat;

let f be PartFunc of (REAL n),REAL;

let x be Element of REAL n;

pred f is_partial_differentiable_in x,i means :: PDIFF_1:def 11

f * (reproj (i,x)) is_differentiable_in (proj (i,n)) . x;

f * (reproj (i,x)) is_differentiable_in (proj (i,n)) . x;

:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 11 :

for n being non zero Nat

for i being Nat

for f being PartFunc of (REAL n),REAL

for x being Element of REAL n holds

( f is_partial_differentiable_in x,i iff f * (reproj (i,x)) is_differentiable_in (proj (i,n)) . x );

for n being non zero Nat

for i being Nat

for f being PartFunc of (REAL n),REAL

for x being Element of REAL n holds

( f is_partial_differentiable_in x,i iff f * (reproj (i,x)) is_differentiable_in (proj (i,n)) . x );

definition

let n be non zero Nat;

let i be Nat;

let f be PartFunc of (REAL n),REAL;

let x be Element of REAL n;

diff ((f * (reproj (i,x))),((proj (i,n)) . x)) is Real ;

end;
let i be Nat;

let f be PartFunc of (REAL n),REAL;

let x be Element of REAL n;

func partdiff (f,x,i) -> Real equals :: PDIFF_1:def 12

diff ((f * (reproj (i,x))),((proj (i,n)) . x));

coherence diff ((f * (reproj (i,x))),((proj (i,n)) . x));

diff ((f * (reproj (i,x))),((proj (i,n)) . x)) is Real ;

:: deftheorem defines partdiff PDIFF_1:def 12 :

for n being non zero Nat

for i being Nat

for f being PartFunc of (REAL n),REAL

for x being Element of REAL n holds partdiff (f,x,i) = diff ((f * (reproj (i,x))),((proj (i,n)) . x));

for n being non zero Nat

for i being Nat

for f being PartFunc of (REAL n),REAL

for x being Element of REAL n holds partdiff (f,x,i) = diff ((f * (reproj (i,x))),((proj (i,n)) . x));

theorem Th12: :: PDIFF_1:12

for n being non zero Nat

for i being Nat

for x being Point of (REAL-NS n)

for y being Element of REAL n st x = y holds

(reproj (i,y)) * (proj (1,1)) = reproj (i,x)

for i being Nat

for x being Point of (REAL-NS n)

for y being Element of REAL n st x = y holds

(reproj (i,y)) * (proj (1,1)) = reproj (i,x)

proof end;

theorem Th13: :: PDIFF_1:13

for n being non zero Nat

for i being Nat

for f being PartFunc of (REAL-NS n),(REAL-NS 1)

for g being PartFunc of (REAL n),REAL

for x being Point of (REAL-NS n)

for y being Element of REAL n st f = <>* g & x = y holds

<>* (g * (reproj (i,y))) = f * (reproj (i,x))

for i being Nat

for f being PartFunc of (REAL-NS n),(REAL-NS 1)

for g being PartFunc of (REAL n),REAL

for x being Point of (REAL-NS n)

for y being Element of REAL n st f = <>* g & x = y holds

<>* (g * (reproj (i,y))) = f * (reproj (i,x))

proof end;

theorem Th14: :: PDIFF_1:14

for n being non zero Nat

for i being Nat

for f being PartFunc of (REAL-NS n),(REAL-NS 1)

for g being PartFunc of (REAL n),REAL

for x being Point of (REAL-NS n)

for y being Element of REAL n st f = <>* g & x = y holds

( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )

for i being Nat

for f being PartFunc of (REAL-NS n),(REAL-NS 1)

for g being PartFunc of (REAL n),REAL

for x being Point of (REAL-NS n)

for y being Element of REAL n st f = <>* g & x = y holds

( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )

proof end;

theorem Th15: :: PDIFF_1:15

for n being non zero Nat

for i being Nat

for f being PartFunc of (REAL-NS n),(REAL-NS 1)

for g being PartFunc of (REAL n),REAL

for x being Point of (REAL-NS n)

for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds

(partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>

for i being Nat

for f being PartFunc of (REAL-NS n),(REAL-NS 1)

for g being PartFunc of (REAL n),REAL

for x being Point of (REAL-NS n)

for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds

(partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>

proof end;

definition

let m, n be non zero Nat;

let i be Nat;

let f be PartFunc of (REAL m),(REAL n);

let x be Element of REAL m;

end;
let i be Nat;

let f be PartFunc of (REAL m),(REAL n);

let x be Element of REAL m;

pred f is_partial_differentiable_in x,i means :: PDIFF_1:def 13

ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & g is_partial_differentiable_in y,i );

ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & g is_partial_differentiable_in y,i );

:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 13 :

for m, n being non zero Nat

for i being Nat

for f being PartFunc of (REAL m),(REAL n)

for x being Element of REAL m holds

( f is_partial_differentiable_in x,i iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & g is_partial_differentiable_in y,i ) );

for m, n being non zero Nat

for i being Nat

for f being PartFunc of (REAL m),(REAL n)

for x being Element of REAL m holds

( f is_partial_differentiable_in x,i iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & g is_partial_differentiable_in y,i ) );

definition

let m, n be non zero Nat;

let i be Nat;

let f be PartFunc of (REAL m),(REAL n);

let x be Element of REAL m;

assume A1: f is_partial_differentiable_in x,i ;

existence

ex b_{1} being Element of REAL n ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & b_{1} = (partdiff (g,y,i)) . <*1*> );

uniqueness

for b_{1}, b_{2} being Element of REAL n st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & b_{1} = (partdiff (g,y,i)) . <*1*> ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & b_{2} = (partdiff (g,y,i)) . <*1*> ) holds

b_{1} = b_{2};

end;
let i be Nat;

let f be PartFunc of (REAL m),(REAL n);

let x be Element of REAL m;

assume A1: f is_partial_differentiable_in x,i ;

func partdiff (f,x,i) -> Element of REAL n means :Def14: :: PDIFF_1:def 14

ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & it = (partdiff (g,y,i)) . <*1*> );

correctness ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & it = (partdiff (g,y,i)) . <*1*> );

existence

ex b

( f = g & x = y & b

uniqueness

for b

( f = g & x = y & b

( f = g & x = y & b

b

proof end;

:: deftheorem Def14 defines partdiff PDIFF_1:def 14 :

for m, n being non zero Nat

for i being Nat

for f being PartFunc of (REAL m),(REAL n)

for x being Element of REAL m st f is_partial_differentiable_in x,i holds

for b_{6} being Element of REAL n holds

( b_{6} = partdiff (f,x,i) iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st

( f = g & x = y & b_{6} = (partdiff (g,y,i)) . <*1*> ) );

for m, n being non zero Nat

for i being Nat

for f being PartFunc of (REAL m),(REAL n)

for x being Element of REAL m st f is_partial_differentiable_in x,i holds

for b

( b

( f = g & x = y & b

theorem :: PDIFF_1:16

theorem Th17: :: PDIFF_1:17

for i being Nat

for m, n being non zero Nat

for F being PartFunc of (REAL-NS m),(REAL-NS n)

for G being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds

(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)

for m, n being non zero Nat

for F being PartFunc of (REAL-NS m),(REAL-NS n)

for G being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds

(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)

proof end;

theorem :: PDIFF_1:18

for n being non zero Nat

for i being Nat

for g being PartFunc of (REAL n),REAL

for y being Element of REAL n

for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds

( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )

for i being Nat

for g being PartFunc of (REAL n),REAL

for y being Element of REAL n

for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds

( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i )

proof end;

theorem :: PDIFF_1:19

for n being non zero Nat

for i being Nat

for g being PartFunc of (REAL n),REAL

for y being Element of REAL n

for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds

partdiff (g1,y,i) = <*(partdiff (g,y,i))*>

for i being Nat

for g being PartFunc of (REAL n),REAL

for y being Element of REAL n

for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds

partdiff (g1,y,i) = <*(partdiff (g,y,i))*>

proof end;

definition

let m, n be non zero Nat;

let i, j be Nat;

let f be PartFunc of (REAL-NS m),(REAL-NS n);

let x be Point of (REAL-NS m);

end;
let i, j be Nat;

let f be PartFunc of (REAL-NS m),(REAL-NS n);

let x be Point of (REAL-NS m);

pred f is_partial_differentiable_in x,i,j means :: PDIFF_1:def 15

((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x;

((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x;

:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 15 :

for m, n being non zero Nat

for i, j being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) holds

( f is_partial_differentiable_in x,i,j iff ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x );

for m, n being non zero Nat

for i, j being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) holds

( f is_partial_differentiable_in x,i,j iff ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x );

definition

let m, n be non zero Nat;

let i, j be Nat;

let f be PartFunc of (REAL-NS m),(REAL-NS n);

let x be Point of (REAL-NS m);

coherence

diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)));

;

end;
let i, j be Nat;

let f be PartFunc of (REAL-NS m),(REAL-NS n);

let x be Point of (REAL-NS m);

func partdiff (f,x,i,j) -> Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) equals :: PDIFF_1:def 16

diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x));

correctness diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x));

coherence

diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)));

;

:: deftheorem defines partdiff PDIFF_1:def 16 :

for m, n being non zero Nat

for i, j being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) holds partdiff (f,x,i,j) = diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x));

for m, n being non zero Nat

for i, j being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) holds partdiff (f,x,i,j) = diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x));

definition

let m, n be non zero Nat;

let i, j be Nat;

let h be PartFunc of (REAL m),(REAL n);

let z be Element of REAL m;

end;
let i, j be Nat;

let h be PartFunc of (REAL m),(REAL n);

let z be Element of REAL m;

pred h is_partial_differentiable_in z,i,j means :: PDIFF_1:def 17

((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z;

((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z;

:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 17 :

for m, n being non zero Nat

for i, j being Nat

for h being PartFunc of (REAL m),(REAL n)

for z being Element of REAL m holds

( h is_partial_differentiable_in z,i,j iff ((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z );

for m, n being non zero Nat

for i, j being Nat

for h being PartFunc of (REAL m),(REAL n)

for z being Element of REAL m holds

( h is_partial_differentiable_in z,i,j iff ((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z );

definition

let m, n be non zero Nat;

let i, j be Nat;

let h be PartFunc of (REAL m),(REAL n);

let z be Element of REAL m;

coherence

diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z)) is Real;

;

end;
let i, j be Nat;

let h be PartFunc of (REAL m),(REAL n);

let z be Element of REAL m;

func partdiff (h,z,i,j) -> Real equals :: PDIFF_1:def 18

diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z));

correctness diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z));

coherence

diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z)) is Real;

;

:: deftheorem defines partdiff PDIFF_1:def 18 :

for m, n being non zero Nat

for i, j being Nat

for h being PartFunc of (REAL m),(REAL n)

for z being Element of REAL m holds partdiff (h,z,i,j) = diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z));

for m, n being non zero Nat

for i, j being Nat

for h being PartFunc of (REAL m),(REAL n)

for z being Element of REAL m holds partdiff (h,z,i,j) = diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z));

theorem :: PDIFF_1:20

theorem :: PDIFF_1:21

for m, n being non zero Nat

for F being PartFunc of (REAL-NS m),(REAL-NS n)

for G being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds

diff (F,x) = diff (G,y)

for F being PartFunc of (REAL-NS m),(REAL-NS n)

for G being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds

diff (F,x) = diff (G,y)

proof end;

theorem Th22: :: PDIFF_1:22

for m, n being non zero Nat

for i, j being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for h being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for z being Element of REAL m st f = h & x = z holds

((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z)))

for i, j being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for h being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for z being Element of REAL m st f = h & x = z holds

((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z)))

proof end;

theorem :: PDIFF_1:23

for m, n being non zero Nat

for i, j being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for h being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for z being Element of REAL m st f = h & x = z holds

( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )

for i, j being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for h being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for z being Element of REAL m st f = h & x = z holds

( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )

proof end;

theorem :: PDIFF_1:24

for m, n being non zero Nat

for i, j being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for h being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds

(partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*>

for i, j being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for h being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds

(partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*>

proof end;

definition

let m, n be non zero Nat;

let i be Nat;

let f be PartFunc of (REAL-NS m),(REAL-NS n);

let X be set ;

end;
let i be Nat;

let f be PartFunc of (REAL-NS m),(REAL-NS n);

let X be set ;

pred f is_partial_differentiable_on X,i means :: PDIFF_1:def 19

( X c= dom f & ( for x being Point of (REAL-NS m) st x in X holds

f | X is_partial_differentiable_in x,i ) );

( X c= dom f & ( for x being Point of (REAL-NS m) st x in X holds

f | X is_partial_differentiable_in x,i ) );

:: deftheorem defines is_partial_differentiable_on PDIFF_1:def 19 :

for m, n being non zero Nat

for i being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for X being set holds

( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Point of (REAL-NS m) st x in X holds

f | X is_partial_differentiable_in x,i ) ) );

for m, n being non zero Nat

for i being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for X being set holds

( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Point of (REAL-NS m) st x in X holds

f | X is_partial_differentiable_in x,i ) ) );

definition

let m, n be non zero Nat;

let i be Nat;

let f be PartFunc of (REAL-NS m),(REAL-NS n);

let X be set ;

assume A1: f is_partial_differentiable_on X,i ;

ex b_{1} being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) st

( dom b_{1} = X & ( for x being Point of (REAL-NS m) st x in X holds

b_{1} /. x = partdiff (f,x,i) ) )

for b_{1}, b_{2} being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) st dom b_{1} = X & ( for x being Point of (REAL-NS m) st x in X holds

b_{1} /. x = partdiff (f,x,i) ) & dom b_{2} = X & ( for x being Point of (REAL-NS m) st x in X holds

b_{2} /. x = partdiff (f,x,i) ) holds

b_{1} = b_{2}

end;
let i be Nat;

let f be PartFunc of (REAL-NS m),(REAL-NS n);

let X be set ;

assume A1: f is_partial_differentiable_on X,i ;

func f `partial| (X,i) -> PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) means :: PDIFF_1:def 20

( dom it = X & ( for x being Point of (REAL-NS m) st x in X holds

it /. x = partdiff (f,x,i) ) );

existence ( dom it = X & ( for x being Point of (REAL-NS m) st x in X holds

it /. x = partdiff (f,x,i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines `partial| PDIFF_1:def 20 :

for m, n being non zero Nat

for i being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for X being set st f is_partial_differentiable_on X,i holds

for b_{6} being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) holds

( b_{6} = f `partial| (X,i) iff ( dom b_{6} = X & ( for x being Point of (REAL-NS m) st x in X holds

b_{6} /. x = partdiff (f,x,i) ) ) );

for m, n being non zero Nat

for i being Nat

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for X being set st f is_partial_differentiable_on X,i holds

for b

( b

b

theorem Th26: :: PDIFF_1:26

for m, n being non zero Nat

for i being Nat

for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) holds

( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) )

for i being Nat

for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) holds

( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) )

proof end;

theorem Th27: :: PDIFF_1:27

for m, n being non zero Nat

for i being Nat

for r being Real

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))

for i being Nat

for r being Real

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x))

proof end;

theorem Th28: :: PDIFF_1:28

for m, n being non zero Nat

for i being Nat

for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds

( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )

for i being Nat

for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds

( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )

proof end;

theorem :: PDIFF_1:29

for n being non zero Nat

for i being Nat

for g1, g2 being PartFunc of (REAL n),REAL

for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds

( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )

for i being Nat

for g1, g2 being PartFunc of (REAL n),REAL

for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds

( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )

proof end;

theorem Th30: :: PDIFF_1:30

for m, n being non zero Nat

for i being Nat

for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds

( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) )

for i being Nat

for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds

( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) )

proof end;

theorem :: PDIFF_1:31

for n being non zero Nat

for i being Nat

for g1, g2 being PartFunc of (REAL n),REAL

for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds

( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )

for i being Nat

for g1, g2 being PartFunc of (REAL n),REAL

for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds

( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )

proof end;

theorem Th32: :: PDIFF_1:32

for m, n being non zero Nat

for i being Nat

for r being Real

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds

( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )

for i being Nat

for r being Real

for f being PartFunc of (REAL-NS m),(REAL-NS n)

for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds

( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )

proof end;

theorem :: PDIFF_1:33

for n being non zero Nat

for i being Nat

for r being Real

for g being PartFunc of (REAL n),REAL

for y being Element of REAL n st g is_partial_differentiable_in y,i holds

( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) )

for i being Nat

for r being Real

for g being PartFunc of (REAL n),REAL

for y being Element of REAL n st g is_partial_differentiable_in y,i holds

( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) )

proof end;