deffunc H₁( Nat, Real) -> Element of REAL = In (((1 / $2) + ((scf r) . ($1 + 1))),REAL);
consider f being Real_Sequence such that
A1: f . 0 = (scf r) . 0 and
A2: for n being Nat holds f . (n + 1) = H₁(n,f . n) from NAT_1:sch 12();
take f ; :: thesis: ( f . 0 = (scf r) . 0 & ( for n being Nat holds f . (n + 1) = (1 / (f . n)) + ((scf r) . (n + 1)) ) )
thus f . 0 = (scf r) . 0 by A1; :: thesis: for n being Nat holds f . (n + 1) = (1 / (f . n)) + ((scf r) . (n + 1))
let n be Nat; :: thesis: f . (n + 1) = (1 / (f . n)) + ((scf r) . (n + 1))
f . (n + 1) = H₁(n,f . n) by A2;
hence f . (n + 1) = (1 / (f . n)) + ((scf r) . (n + 1)) ; :: thesis: verum