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, Def13;
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 10;
then (partdiff g,y,i) . <*1*> is Element of REAL n by FINSEQ_2:118, FUNCT_2:7;
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