reconsider g = f as PartFunc of (REAL n),REAL by REAL_NS1:def 4;

reconsider y = x as Element of REAL n by REAL_NS1:def 4;

REAL n = the carrier of (REAL-NS n) by REAL_NS1:def 4;

then diff (g,y) is Function of (REAL-NS n),REAL ;

hence ex b_{1} being Function of (REAL-NS n),REAL ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st

( f = g & x = y & b_{1} = diff (g,y) )
; :: thesis: verum

reconsider y = x as Element of REAL n by REAL_NS1:def 4;

REAL n = the carrier of (REAL-NS n) by REAL_NS1:def 4;

then diff (g,y) is Function of (REAL-NS n),REAL ;

hence ex b

( f = g & x = y & b