A2: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;
consider g being PartFunc of ,, y being Point of 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 , ex y being Point of 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 , ex y being Point of st
( f = g & x = y & b₁ = (partdiff g,y,i) . <*1*> ) & ex g being PartFunc of , ex y being Point of st
( f = g & x = y & b₂ = (partdiff g,y,i) . <*1*> ) holds
b₁ = b₂ ) ) by A3, A4; :: thesis: verum