set s = scf r;
deffunc H₁( Nat, Real, Real) -> Element of REAL = In (((((scf r) . ($1 + 2)) * $3) + $2),REAL);
reconsider s0 = (scf r) . 0, s1 = (((scf r) . 1) * ((scf r) . 0)) + 1 as Element of REAL by XREAL_0:def 1;
consider f being Real_Sequence such that
A1: ( f . 0 = s0 & f . 1 = s1 ) 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 = (scf r) . 0 & f . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) ) )
thus ( f . 0 = (scf r) . 0 & f . 1 = (((scf r) . 1) * ((scf r) . 0)) + 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