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