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

diff (g,x) is Element of REAL n by REAL_NS1:def 4;

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

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

diff (g,x) is Element of REAL n by REAL_NS1:def 4;

hence ex b

( f = g & b