defpred S1[ set ] means ex m being Element of NAT st $1 = 5 * 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 = (5 * 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[ set ] means ex m being Element of NAT st $1 = (5 * 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[ set ] means ex m being Element of NAT st $1 = (5 * 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[ set ] means ex m being Element of NAT st $1 = (5 * m) + 4;
consider O being Subset of NAT such that
A5: for n being Element of NAT holds
( n in O iff S5[n] ) from SUBSET_1:sch 3();
 defpred S6[ Element of NAT , set ] means ( ( $1 in N implies $2 = F1(($1 / 5)) ) & ( $1 in M implies $2 = F2((($1 - 1) / 5)) ) & ( $1 in K implies $2 = F3((($1 - 2) / 5)) ) & ( $1 in L implies $2 = F4((($1 - 3) / 5)) ) & ( $1 in O implies $2 = F5((($1 - 4) / 5)) ) );
A6: for n being Element of NAT ex r being Real st S6[n,r]
proof
let n be Element of NAT ; :: thesis: ex r being Real st S6[n,r]
consider m being Element of NAT such that
A7: ( n = 5 * m or n = (5 * m) + 1 or n = (5 * m) + 2 or n = (5 * m) + 3 or n = (5 * m) + 4 ) by Th4;
now
per cases ( n = 5 * m or n = (5 * m) + 1 or n = (5 * m) + 2 or n = (5 * m) + 3 or n = (5 * m) + 4 ) by A7;
suppose A8: n = 5 * m ; :: thesis: ex r, r being Real st S6[n,r]
take r = F1((n / 5)); :: thesis: ex r being Real st S6[n,r]
A9: n = (5 * m) + 0 by A8;
A10: now
assume n in K ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 2 by A3;
hence contradiction by A9, NAT_1:18; :: thesis: verum
end;
A11: now
assume n in O ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 4 by A5;
hence contradiction by A9, NAT_1:18; :: thesis: verum
end;
A12: now
assume n in L ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 3 by A4;
hence contradiction by A9, NAT_1:18; :: thesis: verum
end;
now
assume n in M ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 1 by A2;
hence contradiction by A9, NAT_1:18; :: thesis: verum
end;
hence ex r being Real st S6[n,r] by A10, A12, A11; :: thesis: verum
end;
suppose A13: n = (5 * m) + 1 ; :: thesis: ex r, r being Real st S6[n,r]
A14: now
assume n in O ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 4 by A5;
hence contradiction by A13, NAT_1:18; :: thesis: verum
end;
A15: now
assume n in L ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 3 by A4;
hence contradiction by A13, NAT_1:18; :: thesis: verum
end;
take r = F2(((n - 1) / 5)); :: thesis: ex r being Real st S6[n,r]
A16: now
assume n in N ; :: thesis: contradiction
then consider k being Element of NAT such that
A17: n = 5 * k by A1;
n = (5 * k) + 0 by A17;
hence contradiction by A13, NAT_1:18; :: thesis: verum
end;
now
assume n in K ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 2 by A3;
hence contradiction by A13, NAT_1:18; :: thesis: verum
end;
hence ex r being Real st S6[n,r] by A16, A15, A14; :: thesis: verum
end;
suppose A18: n = (5 * m) + 2 ; :: thesis: ex r, r being Real st S6[n,r]
A19: now
assume n in O ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 4 by A5;
hence contradiction by A18, NAT_1:18; :: thesis: verum
end;
A20: now
assume n in L ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 3 by A4;
hence contradiction by A18, NAT_1:18; :: thesis: verum
end;
take r = F3(((n - 2) / 5)); :: thesis: ex r being Real st S6[n,r]
A21: now
assume n in N ; :: thesis: contradiction
then consider k being Element of NAT such that
A22: n = 5 * k by A1;
n = (5 * k) + 0 by A22;
hence contradiction by A18, NAT_1:18; :: thesis: verum
end;
now
assume n in M ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 1 by A2;
hence contradiction by A18, NAT_1:18; :: thesis: verum
end;
hence ex r being Real st S6[n,r] by A21, A20, A19; :: thesis: verum
end;
suppose A23: n = (5 * m) + 3 ; :: thesis: ex r, r being Real st S6[n,r]
A24: now
assume n in O ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 4 by A5;
hence contradiction by A23, NAT_1:18; :: thesis: verum
end;
A25: now
assume n in K ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 2 by A3;
hence contradiction by A23, NAT_1:18; :: thesis: verum
end;
take r = F4(((n - 3) / 5)); :: thesis: ex r being Real st S6[n,r]
A26: now
assume n in N ; :: thesis: contradiction
then consider k being Element of NAT such that
A27: n = 5 * k by A1;
n = (5 * k) + 0 by A27;
hence contradiction by A23, NAT_1:18; :: thesis: verum
end;
now
assume n in M ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 1 by A2;
hence contradiction by A23, NAT_1:18; :: thesis: verum
end;
hence ex r being Real st S6[n,r] by A26, A25, A24; :: thesis: verum
end;
suppose A28: n = (5 * m) + 4 ; :: thesis: ex r, r being Real st S6[n,r]
A29: now
assume n in L ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 3 by A4;
hence contradiction by A28, NAT_1:18; :: thesis: verum
end;
A30: now
assume n in K ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 2 by A3;
hence contradiction by A28, NAT_1:18; :: thesis: verum
end;
take r = F5(((n - 4) / 5)); :: thesis: ex r being Real st S6[n,r]
A31: now
assume n in N ; :: thesis: contradiction
then consider k being Element of NAT such that
A32: n = 5 * k by A1;
n = (5 * k) + 0 by A32;
hence contradiction by A28, NAT_1:18; :: thesis: verum
end;
now
assume n in M ; :: thesis: contradiction
then ex k being Element of NAT st n = (5 * k) + 1 by A2;
hence contradiction by A28, NAT_1:18; :: thesis: verum
end;
hence ex r being Real st S6[n,r] by A31, A30, A29; :: thesis: verum
end;
end;
end;
hence ex r being Real st S6[n,r] ; :: thesis: verum
end;
consider f being Function of NAT,REAL such that
A33: for n being Element of NAT holds S6[n,f . n] from FUNCT_2:sch 3(A6);
 reconsider f = f as Real_Sequence ;
take f ; :: thesis: for n being Element of NAT holds
( f . (5 * n) = F1(n) & f . ((5 * n) + 1) = F2(n) & f . ((5 * n) + 2) = F3(n) & f . ((5 * n) + 3) = F4(n) & f . ((5 * n) + 4) = F5(n) )
let n be Element of NAT ; :: thesis: ( f . (5 * n) = F1(n) & f . ((5 * n) + 1) = F2(n) & f . ((5 * n) + 2) = F3(n) & f . ((5 * n) + 3) = F4(n) & f . ((5 * n) + 4) = F5(n) )
5 * n in N by A1;
hence f . (5 * n) = F1(((5 * n) / 5)) by A33
.= F1(n) ;
:: thesis: ( f . ((5 * n) + 1) = F2(n) & f . ((5 * n) + 2) = F3(n) & f . ((5 * n) + 3) = F4(n) & f . ((5 * n) + 4) = F5(n) )
(5 * n) + 1 in M by A2;
hence f . ((5 * n) + 1) = F2(((((5 * n) + 1) - 1) / 5)) by A33
.= F2(n) ;
:: thesis: ( f . ((5 * n) + 2) = F3(n) & f . ((5 * n) + 3) = F4(n) & f . ((5 * n) + 4) = F5(n) )
(5 * n) + 2 in K by A3;
hence f . ((5 * n) + 2) = F3(((((5 * n) + 2) - 2) / 5)) by A33
.= F3(n) ;
:: thesis: ( f . ((5 * n) + 3) = F4(n) & f . ((5 * n) + 4) = F5(n) )
(5 * n) + 3 in L by A4;
hence f . ((5 * n) + 3) = F4(((((5 * n) + 3) - 3) / 5)) by A33
.= F4(n) ;
:: thesis: f . ((5 * n) + 4) = F5(n)
(5 * n) + 4 in O by A5;
hence f . ((5 * n) + 4) = F5(((((5 * n) + 4) - 4) / 5)) by A33
.= F5(n) ;
:: thesis: verum