consider g being PartFunc of (REAL-NS m),(REAL-NS n), y being Point of (REAL-NS m) such that
A2: ( f = g & x = y & g is_differentiable_in y ) by A1, Def7;
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then diff g,y is Function of (REAL m),(REAL n) by LOPBAN_1:def 10;
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 A2; :: thesis: verum