deffunc H₁( Nat, Real, Real) -> Element of REAL = In (((((scf r) . ($1 + 2)) * $3) + $2),REAL);
let f, g be Real_Sequence; :: 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) ) & g . 0 = 1 & g . 1 = (scf r) . 1 & ( for n being Nat holds g . (n + 2) = (((scf r) . (n + 2)) * (g . (n + 1))) + (g . n) ) implies f = g )
assume that
A3: ( f . 0 = 1 & f . 1 = (scf r) . 1 ) and
A4: for k being Nat holds f . (k + 2) = (((scf r) . (k + 2)) * (f . (k + 1))) + (f . k) and
A5: ( g . 0 = 1 & g . 1 = (scf r) . 1 ) and
A6: for k being Nat holds g . (k + 2) = (((scf r) . (k + 2)) * (g . (k + 1))) + (g . k) ; :: thesis: f = g
A7: ( g . 0 = jj & g . 1 = (scf r) . 1 ) by A5;
A8: for k being Nat holds g . (k + 2) = H₁(k,g . k,g . (k + 1)) by A6;
A9: for k being Nat holds f . (k + 2) = H₁(k,f . k,f . (k + 1)) by A4;
A10: ( f . 0 = jj & f . 1 = (scf r) . 1 ) by A3;
f = g from RECDEF_2:sch 7(A10, A9, A7, A8);
hence f = g ; :: thesis: verum