defpred S1[ set ] means ex m being Element of NAT st $1 = 3 * m;
consider E being Subset of NAT such that
A1: for n being Element of NAT holds
( n in E iff S1[n] ) from SUBSET_1:sch 3();
 defpred S2[ set ] means ex m being Element of NAT st $1 = (3 * m) + 1;
consider G being Subset of NAT such that
A2: for n being Element of NAT holds
( n in G iff S2[n] ) from SUBSET_1:sch 3();
 defpred S3[ set ] means ex m being Element of NAT st $1 = (3 * m) + 2;
consider K being Subset of NAT such that
A3: for n being Element of NAT holds
( n in K iff S3[n] ) from SUBSET_1:sch 3();
 defpred S4[ Element of NAT , set ] means ( ( $1 in E implies $2 = F1(($1 / 3)) ) & ( $1 in G implies $2 = F2((($1 - 1) / 3)) ) & ( $1 in K implies $2 = F3((($1 - 2) / 3)) ) );
A4: for n being Element of NAT ex r being Element of REAL st S4[n,r]
proof
let n be Element of NAT ; :: thesis: ex r being Element of REAL st S4[n,r]
consider m being Element of NAT such that
A5: ( n = 3 * m or n = (3 * m) + 1 or n = (3 * m) + 2 ) by Th2;
now :: thesis: ex r, r being Element of REAL st S4[n,r]
per cases ( n = 3 * m or n = (3 * m) + 1 or n = (3 * m) + 2 ) by A5;
suppose A6: n = 3 * m ; :: thesis: ex r, r being Element of REAL st S4[n,r]
take r = F1((n / 3)); :: thesis: ex r being Element of REAL st S4[n,r]
A7: n = (3 * m) + 0 by A6;
A8: now :: thesis: not n in K
assume n in K ; :: thesis: contradiction
then ex k being Element of NAT st n = (3 * k) + 2 by A3;
hence contradiction by A7, NAT_1:18; :: thesis: verum
end;
now :: thesis: not n in G
assume n in G ; :: thesis: contradiction
then ex k being Element of NAT st n = (3 * k) + 1 by A2;
hence contradiction by A7, NAT_1:18; :: thesis: verum
end;
hence ex r being Element of REAL st S4[n,r] by A8; :: thesis: verum
end;
suppose A9: n = (3 * m) + 1 ; :: thesis: ex r, r being Element of REAL st S4[n,r]
take r = F2(((n - 1) / 3)); :: thesis: ex r being Element of REAL st S4[n,r]
A10: now :: thesis: not n in E
assume n in E ; :: thesis: contradiction
then consider k being Element of NAT such that
A11: n = 3 * k by A1;
n = (3 * k) + 0 by A11;
hence contradiction by A9, NAT_1:18; :: thesis: verum
end;
now :: thesis: not n in K
assume n in K ; :: thesis: contradiction
then ex k being Element of NAT st n = (3 * k) + 2 by A3;
hence contradiction by A9, NAT_1:18; :: thesis: verum
end;
hence ex r being Element of REAL st S4[n,r] by A10; :: thesis: verum
end;
suppose A12: n = (3 * m) + 2 ; :: thesis: ex r, r being Element of REAL st S4[n,r]
take r = F3(((n - 2) / 3)); :: thesis: ex r being Element of REAL st S4[n,r]
A13: now :: thesis: not n in E
assume n in E ; :: thesis: contradiction
then consider k being Element of NAT such that
A14: n = 3 * k by A1;
n = (3 * k) + 0 by A14;
hence contradiction by A12, NAT_1:18; :: thesis: verum
end;
now :: thesis: not n in G
assume n in G ; :: thesis: contradiction
then ex k being Element of NAT st n = (3 * k) + 1 by A2;
hence contradiction by A12, NAT_1:18; :: thesis: verum
end;
hence ex r being Element of REAL st S4[n,r] by A13; :: thesis: verum
end;
end;
end;
hence ex r being Element of REAL st S4[n,r] ; :: thesis: verum
end;
consider f being sequence of REAL such that
A15: for n being Element of NAT holds S4[n,f . n] from FUNCT_2:sch 3(A4);
 reconsider f = f as Real_Sequence ;
take f ; :: thesis: for n being Element of NAT holds
( f . (3 * n) = F1(n) & f . ((3 * n) + 1) = F2(n) & f . ((3 * n) + 2) = F3(n) )
let n be Element of NAT ; :: thesis: ( f . (3 * n) = F1(n) & f . ((3 * n) + 1) = F2(n) & f . ((3 * n) + 2) = F3(n) )
3 * n in E by A1;
hence f . (3 * n) = F1(((3 * n) / 3)) by A15
.= F1(n) ;
:: thesis: ( f . ((3 * n) + 1) = F2(n) & f . ((3 * n) + 2) = F3(n) )
(3 * n) + 1 in G by A2;
hence f . ((3 * n) + 1) = F2(((((3 * n) + 1) - 1) / 3)) by A15
.= F2(n) ;
:: thesis: f . ((3 * n) + 2) = F3(n)
(3 * n) + 2 in K by A3;
hence f . ((3 * n) + 2) = F3(((((3 * n) + 2) - 2) / 3)) by A15
.= F3(n) ;
:: thesis: verum