defpred S₁[ set ] means ex m being Nat st $1 = 2 * m;
consider N being Subset of NAT such that
A1: for n being Element of NAT holds
( n in N iff S₁[n] ) from SUBSET_1:sch 3();
defpred S₂[ set ] means ex m being Nat st $1 = (2 * m) + 1;
consider M being Subset of NAT such that
A2: for n being Element of NAT holds
( n in M iff S₂[n] ) from SUBSET_1:sch 3();
defpred S₃[ Nat, set ] means ( ( $1 in N implies $2 = F₂(($1 / 2)) ) & ( $1 in M implies $2 = F₃((($1 - 1) / 2)) ) );
A3: for n being Element of NAT ex r being Element of F₁() st S₃[n,r]

proof

let n be Element of NAT ; :: thesis: ex r being Element of F₁() st S₃[n,r]

now :: thesis: ( n in N implies ex r being Element of F₁() st not n in M )

assume A4: n in N ; :: thesis: not for r being Element of F₁() holds n in M
reconsider r = F₂((n / 2)) as Element of F₁() ;
take r = r; :: thesis: not n in M

hereby :: thesis: verum

assume n in M ; :: thesis: contradiction
then A5: ex k being Nat st n = (2 * k) + 1 by A2;
ex m being Nat st n = 2 * m by A1, A4;
hence contradiction by A5; :: thesis: verum

end;

end;

hence ex r being Element of F₁() st S₃[n,r] ; :: thesis: verum

end;

consider f being sequence of F₁() such that
A6: for n being Element of NAT holds S₃[n,f . n] from FUNCT_2:sch 3(A3);
reconsider f = f as sequence of F₁() ;
take f ; :: thesis: for n being Nat holds
( f . (2 * n) = F₂(n) & f . ((2 * n) + 1) = F₃(n) )
let n be Nat; :: thesis: ( f . (2 * n) = F₂(n) & f . ((2 * n) + 1) = F₃(n) )
reconsider m = 2 * n as Nat ;
A7: m in NAT by ORDINAL1:def 12;
f . ((2 * n) + 1) = F₃(((((2 * n) + 1) - 1) / 2)) by A6, A2;
hence ( f . (2 * n) = F₂(n) & f . ((2 * n) + 1) = F₃(n) ) by A1, A6, A7; :: thesis: verum