consider f being sequence of INT such that
A1: ( f . 0 = j & f . 1 = z & ( for n being Nat holds f . (n + 2) = H₁(n,f . n,f . (n + 1)) ) ) from RECDEF_2:sch 5();
take f ; :: thesis: ( f . 0 = 1 & f . 1 = 0 & ( for n being Nat holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) ) )
thus ( f . 0 = 1 & f . 1 = 0 ) by A1; :: thesis: for n being Nat holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1)))
let n be Nat; :: thesis: f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1)))
f . (n + 2) = H₁(n,f . n,f . (n + 1)) by A1;
hence f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) ; :: thesis: verum