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_differentiable_in y by A1;
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 9;
hence ( ex b₁ being Function of (REAL m),(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₁ = diff (g,y) ) & ( for b₁, b₂ being Function of (REAL m),(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₁ = diff (g,y) ) & 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₂ = diff (g,y) ) holds
b₁ = b₂ ) ) by A3, A4; :: thesis: verum