consider f being Function such that
A1: dom f = NAT and
A2: ( f . 0 = F₂() & f . 1 = F₃() & f . 2 = F₄() & f . 3 = F₅() ) and
A3: for n being Element of NAT holds f . (n + 4) = F₆(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3))) from RECDEF_2:sch 12();
rng f c= F₁()

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in F₁() )
assume y in rng f ; :: thesis: y in F₁()
then consider n being set such that
A4: n in dom f and
A5: f . n = y by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A1, A4;

per cases ( n <= 3 or n > 3 ) ;

suppose n <= 3 ; :: thesis: y in F₁()

then ( n = 0 or n = 1 or n = 2 or n = 3 ) by NAT_1:28;
hence y in F₁() by A2, A5; :: thesis: verum

end;

suppose n > 3 ; :: thesis: y in F₁()

then 3 + 1 <= n by NAT_1:13;
then n - 4 is Element of NAT by INT_1:18;
then f . ((n - 4) + 4) = F₆((n - 4),(f . (n - 4)),(f . ((n - 4) + 1)),(f . ((n - 4) + 2)),(f . ((n - 4) + 3))) by A3;
hence y in F₁() by A5; :: thesis: verum

end;

end;

end;

then f is Function of NAT ,F₁() by A1, FUNCT_2:def 1, RELSET_1:11;
hence ex f being Function of NAT ,F₁() st
( f . 0 = F₂() & f . 1 = F₃() & f . 2 = F₄() & f . 3 = F₅() & ( for n being Element of NAT holds f . (n + 4) = F₆(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3))) ) ) by A2, A3; :: thesis: verum