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₁ 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₁ = (partdiff (g,y,i)) . <*1*> ) & ( for b₁, b₂ 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₁ = (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₂ = (partdiff (g,y,i)) . <*1*> ) holds
b₁ = b₂ ) ) by A3, A4; :: thesis: verum