consider f being Function such that
A1: dom f = NAT and
A2: ( f . 0 = F2() & f . 1 = F3() ) and
A3: for n being Nat holds f . (n + 2) = F4(n,(f . n),(f . (n + 1))) from RECDEF_2:sch 4();
 rng f c= F1()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in F1() )
assume y in rng f ; :: thesis: y in F1()
then consider n being object such that
A4: n in dom f and
A5: f . n = y by FUNCT_1:def 3;
reconsider n = n as Nat by A1, A4;
per cases ( n <= 1 or n > 1 ) ;
suppose n <= 1 ; :: thesis: y in F1()
then ( n = 0 or n = 1 ) by NAT_1:25;
hence y in F1() by A2, A5; :: thesis: verum
end;
suppose n > 1 ; :: thesis: y in F1()
then 1 + 1 <= n by NAT_1:13;
then n - 2 in NAT by INT_1:5;
then f . ((n - 2) + 2) = F4((n - 2),(f . (n - 2)),(f . ((n - 2) + 1))) by A3;
hence y in F1() by A5; :: thesis: verum
end;
end;
end;
then f is sequence of F1() by A1, FUNCT_2:def 1, RELSET_1:4;
hence ex f being sequence of F1() st
( f . 0 = F2() & f . 1 = F3() & ( for n being Nat holds f . (n + 2) = F4(n,(f . n),(f . (n + 1))) ) ) by A2, A3; :: thesis: verum