defpred S1[ set ] means ex m being Element of 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 S1[n] ) from SUBSET_1:sch 3();
 defpred S2[ set ] means ex m being Element of 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 S2[n] ) from SUBSET_1:sch 3();
 defpred S3[ Element of NAT , set ] means ( ( $1 in N implies $2 = F1(($1 / 2)) ) & ( $1 in M implies $2 = F2((($1 - 1) / 2)) ) );
A3: for n being Element of NAT ex r being Real st S3[n,r]
proof
let n be Element of NAT ; :: thesis: ex r being Real st S3[n,r]
now
assume A4: n in N ; :: thesis: ex r, r being Real st S3[n,r]
take r = F1((n / 2)); :: thesis: ex r being Real st S3[n,r]
now
assume n in M ; :: thesis: contradiction
then A5: ex k being Element of NAT st n = (2 * k) + 1 by A2;
consider m being Element of NAT such that
A6: n = 2 * m by A1, A4;
n = (2 * m) + 0 by A6;
hence contradiction by A5, NAT_1:18; :: thesis: verum
end;
hence ex r being Real st S3[n,r] ; :: thesis: verum
end;
hence ex r being Real st S3[n,r] ; :: thesis: verum
end;
consider f being Function of NAT,REAL such that
A7: for n being Element of NAT holds S3[n,f . n] from FUNCT_2:sch 3(A3);
 reconsider f = f as Real_Sequence ;
take f ; :: thesis: for n being Element of NAT holds
( f . (2 * n) = F1(n) & f . ((2 * n) + 1) = F2(n) )
let n be Element of NAT ; :: thesis: ( f . (2 * n) = F1(n) & f . ((2 * n) + 1) = F2(n) )
2 * n in N by A1;
hence f . (2 * n) = F1(((2 * n) / 2)) by A7
.= F1(n) ;
:: thesis: f . ((2 * n) + 1) = F2(n)
(2 * n) + 1 in M by A2;
hence f . ((2 * n) + 1) = F2(((((2 * n) + 1) - 1) / 2)) by A7
.= F2(n) ;
:: thesis: verum