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_differentiable_in y by A1, Def7;
the carrier of (REAL-NS m) = REAL m by REAL_NS1:def 4;
then diff g,y is Function of REAL m, REAL n by A2, LOPBAN_1:def 10;
hence ( ex b₁ being Function of REAL m, REAL n ex g being PartFunc of , ex y being Point of st
( f = g & x = y & b₁ = diff g,y ) & ( for b₁, b₂ being Function of REAL m, REAL n st ex g being PartFunc of , ex y being Point of st
( f = g & x = y & b₁ = diff g,y ) & ex g being PartFunc of , ex y being Point of st
( f = g & x = y & b₂ = diff g,y ) holds
b₁ = b₂ ) ) by A3, A4; :: thesis: verum