let F, G be Field; :: thesis: for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat holds (fdif (f,h)) . n is Function of V,W

let V be VectSp of F; :: thesis: for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat holds (fdif (f,h)) . n is Function of V,W

let W be VectSp of G; :: thesis: for f being Function of V,W

for h being Element of V

for n being Nat holds (fdif (f,h)) . n is Function of V,W

let f be Function of V,W; :: thesis: for h being Element of V

for n being Nat holds (fdif (f,h)) . n is Function of V,W

let h be Element of V; :: thesis: for n being Nat holds (fdif (f,h)) . n is Function of V,W

defpred S_{1}[ Nat] means (fdif (f,h)) . $1 is Function of V,W;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by Def6;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A2, A1);

hence for n being Nat holds (fdif (f,h)) . n is Function of V,W ; :: thesis: verum

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat holds (fdif (f,h)) . n is Function of V,W

let V be VectSp of F; :: thesis: for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat holds (fdif (f,h)) . n is Function of V,W

let W be VectSp of G; :: thesis: for f being Function of V,W

for h being Element of V

for n being Nat holds (fdif (f,h)) . n is Function of V,W

let f be Function of V,W; :: thesis: for h being Element of V

for n being Nat holds (fdif (f,h)) . n is Function of V,W

let h be Element of V; :: thesis: for n being Nat holds (fdif (f,h)) . n is Function of V,W

defpred S

A1: for k being Nat st S

S

proof

A2:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume (fdif (f,h)) . k is Function of V,W ; :: thesis: S_{1}[k + 1]

then fD (((fdif (f,h)) . k),h) is Function of V,W ;

hence S_{1}[k + 1]
by Def6; :: thesis: verum

end;assume (fdif (f,h)) . k is Function of V,W ; :: thesis: S

then fD (((fdif (f,h)) . k),h) is Function of V,W ;

hence S

for n being Nat holds S

hence for n being Nat holds (fdif (f,h)) . n is Function of V,W ; :: thesis: verum