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₁ being Element of REAL n ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & b₁ = diff (g,x) ) ; :: thesis: verum