let f, g be sequence of INT; :: thesis: ( f . 0 = 1 & f . 1 = 0 & ( for n being Nat holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) ) & g . 0 = 1 & g . 1 = 0 & ( for n being Nat holds g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) ) implies f = g )
assume ( f . 0 = 1 & f . 1 = 0 ) ; :: thesis: ( ex n being Nat st not f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) or not g . 0 = 1 or not g . 1 = 0 or ex n being Nat st not g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) or f = g )
then A2: ( f . 0 = j & f . 1 = z ) ;
assume for n being Nat holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) ; :: thesis: ( not g . 0 = 1 or not g . 1 = 0 or ex n being Nat st not g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) or f = g )
then A3: for n being Nat holds f . (n + 2) = H₁(n,f . n,f . (n + 1)) ;
assume ( g . 0 = 1 & g . 1 = 0 ) ; :: thesis: ( ex n being Nat st not g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) or f = g )
then A4: ( g . 0 = j & g . 1 = z ) ;
assume for n being Nat holds g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) ; :: thesis: f = g
then A5: for n being Nat holds g . (n + 2) = H₁(n,g . n,g . (n + 1)) ;
thus f = g from RECDEF_2:sch 7(A2, A3, A4, A5); :: thesis: verum