deffunc H₁( Nat, Real, Real) -> Element of REAL = In (((((scf r) . ($1 + 2)) * $3) + $2),REAL);
consider f being Real_Sequence such that
A1: ( f . 0 = jj & f . 1 = (scf r) . 1 ) and
A2: 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 = (scf r) . 1 & ( for n being Nat holds f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) ) )
thus ( f . 0 = 1 & f . 1 = (scf r) . 1 ) by A1; :: thesis: for n being Nat holds f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n)
let n be Nat; :: thesis: f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n)
f . (n + 2) = H₁(n,f . n,f . (n + 1)) by A2;
hence f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) ; :: thesis: verum