let n be non zero Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n)

for h being PartFunc of REAL,(REAL-NS n)

for x being Real st h = f holds

diff (f,x) = diff (h,x)

let f be PartFunc of REAL,(REAL n); :: thesis: for h being PartFunc of REAL,(REAL-NS n)

for x being Real st h = f holds

diff (f,x) = diff (h,x)

let h be PartFunc of REAL,(REAL-NS n); :: thesis: for x being Real st h = f holds

diff (f,x) = diff (h,x)

let x be Real; :: thesis: ( h = f implies diff (f,x) = diff (h,x) )

ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & diff (f,x) = diff (g,x) ) by Def2;

hence ( h = f implies diff (f,x) = diff (h,x) ) ; :: thesis: verum

for h being PartFunc of REAL,(REAL-NS n)

for x being Real st h = f holds

diff (f,x) = diff (h,x)

let f be PartFunc of REAL,(REAL n); :: thesis: for h being PartFunc of REAL,(REAL-NS n)

for x being Real st h = f holds

diff (f,x) = diff (h,x)

let h be PartFunc of REAL,(REAL-NS n); :: thesis: for x being Real st h = f holds

diff (f,x) = diff (h,x)

let x be Real; :: thesis: ( h = f implies diff (f,x) = diff (h,x) )

ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & diff (f,x) = diff (g,x) ) by Def2;

hence ( h = f implies diff (f,x) = diff (h,x) ) ; :: thesis: verum