A2:
the carrier of (REAL-NS n) = REAL n
by REAL_NS1:def 4;

consider g being PartFunc of (REAL-NS m),(REAL-NS n), y being Point of (REAL-NS m) such that

A3: f = g and

A4: x = y and

g is_partial_differentiable_in y,i by A1;

the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

then partdiff (g,y,i) is Function of (REAL 1),(REAL n) by A2, LOPBAN_1:def 9;

then (partdiff (g,y,i)) . <*jj*> is Element of REAL n by FINSEQ_2:98, FUNCT_2:5;

hence ( 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*> ) & ( 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} ) )
by A3, A4; :: thesis: verum

consider g being PartFunc of (REAL-NS m),(REAL-NS n), y being Point of (REAL-NS m) such that

A3: f = g and

A4: x = y and

g is_partial_differentiable_in y,i by A1;

the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

then partdiff (g,y,i) is Function of (REAL 1),(REAL n) by A2, LOPBAN_1:def 9;

then (partdiff (g,y,i)) . <*jj*> is Element of REAL n by FINSEQ_2:98, FUNCT_2:5;

hence ( ex b

( f = g & x = y & b

( f = g & x = y & b

( f = g & x = y & b

b