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₁ 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₁ = diff (g,y) ) ; :: thesis: verum