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_{1} 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_{1} = diff (g,y) ) & ( for b_{1}, b_{2} 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_{1} = 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_{2} = diff (g,y) ) holds

b_{1} = b_{2} ) )
by A3, A4; :: thesis: verum

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

( f = g & x = y & b

( f = g & x = y & b

( f = g & x = y & b

b