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