consider f being Function of NAT,INT such that
A1: ( f . 0 = j & f . 1 = z & ( for n being Element of 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 = 0 & ( for n being natural number holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) ) )
thus ( f . 0 = 1 & f . 1 = 0 ) by A1; :: thesis: for n being natural number holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1)))
let n be natural number ; :: thesis: f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1)))
n is Element of NAT by ORDINAL1:def 12;
hence f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) by A1; :: thesis: verum