consider f being Function such that

A1: dom f = NAT and

A2: ( f . 0 = F_{2}() & f . 1 = F_{3}() )
and

A3: for n being Nat holds f . (n + 2) = F_{4}(n,(f . n),(f . (n + 1)))
from RECDEF_2:sch 4();

rng f c= F_{1}()
_{1}()
by A1, FUNCT_2:def 1, RELSET_1:4;

hence ex f being sequence of F_{1}() st

( f . 0 = F_{2}() & f . 1 = F_{3}() & ( for n being Nat holds f . (n + 2) = F_{4}(n,(f . n),(f . (n + 1))) ) )
by A2, A3; :: thesis: verum

A1: dom f = NAT and

A2: ( f . 0 = F

A3: for n being Nat holds f . (n + 2) = F

rng f c= F

proof

then
f is sequence of F
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in F_{1}() )

assume y in rng f ; :: thesis: y in F_{1}()

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;

end;assume y in rng f ; :: thesis: y in F

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;

hence ex f being sequence of F

( f . 0 = F