defpred S_{1}[ 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 S_{1}[n] )
from SUBSET_1:sch 3();

defpred S_{2}[ 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 S_{2}[n] )
from SUBSET_1:sch 3();

defpred S_{3}[ 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 S_{3}[n] )
from SUBSET_1:sch 3();

defpred S_{4}[ 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 S_{4}[n] )
from SUBSET_1:sch 3();

defpred S_{5}[ 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 S_{5}[n] )
from SUBSET_1:sch 3();

defpred S_{6}[ Element of NAT , set ] means ( ( $1 in N implies $2 = F_{1}(($1 / 5)) ) & ( $1 in M implies $2 = F_{2}((($1 - 1) / 5)) ) & ( $1 in K implies $2 = F_{3}((($1 - 2) / 5)) ) & ( $1 in L implies $2 = F_{4}((($1 - 3) / 5)) ) & ( $1 in O implies $2 = F_{5}((($1 - 4) / 5)) ) );

A6: for n being Element of NAT ex r being Element of REAL st S_{6}[n,r]

A33: for n being Element of NAT holds S_{6}[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) = F_{1}(n) & f . ((5 * n) + 1) = F_{2}(n) & f . ((5 * n) + 2) = F_{3}(n) & f . ((5 * n) + 3) = F_{4}(n) & f . ((5 * n) + 4) = F_{5}(n) )

let n be Element of NAT ; :: thesis: ( f . (5 * n) = F_{1}(n) & f . ((5 * n) + 1) = F_{2}(n) & f . ((5 * n) + 2) = F_{3}(n) & f . ((5 * n) + 3) = F_{4}(n) & f . ((5 * n) + 4) = F_{5}(n) )

5 * n in N by A1;

hence f . (5 * n) = F_{1}(((5 * n) / 5))
by A33

.= F_{1}(n)
;

:: thesis: ( f . ((5 * n) + 1) = F_{2}(n) & f . ((5 * n) + 2) = F_{3}(n) & f . ((5 * n) + 3) = F_{4}(n) & f . ((5 * n) + 4) = F_{5}(n) )

(5 * n) + 1 in M by A2;

hence f . ((5 * n) + 1) = F_{2}(((((5 * n) + 1) - 1) / 5))
by A33

.= F_{2}(n)
;

:: thesis: ( f . ((5 * n) + 2) = F_{3}(n) & f . ((5 * n) + 3) = F_{4}(n) & f . ((5 * n) + 4) = F_{5}(n) )

(5 * n) + 2 in K by A3;

hence f . ((5 * n) + 2) = F_{3}(((((5 * n) + 2) - 2) / 5))
by A33

.= F_{3}(n)
;

:: thesis: ( f . ((5 * n) + 3) = F_{4}(n) & f . ((5 * n) + 4) = F_{5}(n) )

(5 * n) + 3 in L by A4;

hence f . ((5 * n) + 3) = F_{4}(((((5 * n) + 3) - 3) / 5))
by A33

.= F_{4}(n)
;

:: thesis: f . ((5 * n) + 4) = F_{5}(n)

(5 * n) + 4 in O by A5;

hence f . ((5 * n) + 4) = F_{5}(((((5 * n) + 4) - 4) / 5))
by A33

.= F_{5}(n)
;

:: thesis: verum

consider N being Subset of NAT such that

A1: for n being Element of NAT holds

( n in N iff S

defpred S

consider M being Subset of NAT such that

A2: for n being Element of NAT holds

( n in M iff S

defpred S

consider K being Subset of NAT such that

A3: for n being Element of NAT holds

( n in K iff S

defpred S

consider L being Subset of NAT such that

A4: for n being Element of NAT holds

( n in L iff S

defpred S

consider O being Subset of NAT such that

A5: for n being Element of NAT holds

( n in O iff S

defpred S

A6: for n being Element of NAT ex r being Element of REAL st S

proof

consider f being sequence of REAL such that
let n be Element of NAT ; :: thesis: ex r being Element of REAL st S_{6}[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;

_{6}[n,r]
; :: thesis: verum

end;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 :: thesis: ex r, r being Element of REAL st S_{6}[n,r]end;

hence
ex r being Element of REAL st Sper 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;

end;

suppose A8:
n = 5 * m
; :: thesis: ex r, r being Element of REAL st S_{6}[n,r]

take r = F_{1}((n / 5)); :: thesis: ex r being Element of REAL st S_{6}[n,r]

A9: n = (5 * m) + 0 by A8;

_{6}[n,r]
by A10, A12, A11; :: thesis: verum

end;A9: n = (5 * m) + 0 by A8;

A10: now :: thesis: not n in K

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;then ex k being Element of NAT st n = (5 * k) + 2 by A3;

hence contradiction by A9, NAT_1:18; :: thesis: verum

A11: now :: thesis: not n in O

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;then ex k being Element of NAT st n = (5 * k) + 4 by A5;

hence contradiction by A9, NAT_1:18; :: thesis: verum

A12: now :: thesis: not n in L

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;then ex k being Element of NAT st n = (5 * k) + 3 by A4;

hence contradiction by A9, NAT_1:18; :: thesis: verum

now :: thesis: not n in M

hence
ex r being Element of REAL st Sassume
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;then ex k being Element of NAT st n = (5 * k) + 1 by A2;

hence contradiction by A9, NAT_1:18; :: thesis: verum

suppose A13:
n = (5 * m) + 1
; :: thesis: ex r, r being Element of REAL st S_{6}[n,r]

_{2}(((n - 1) / 5)); :: thesis: ex r being Element of REAL st S_{6}[n,r]

_{6}[n,r]
by A16, A15, A14; :: thesis: verum

end;

A14: now :: thesis: not n in O

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;then ex k being Element of NAT st n = (5 * k) + 4 by A5;

hence contradiction by A13, NAT_1:18; :: thesis: verum

A15: now :: thesis: not n in L

take r = Fassume
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;then ex k being Element of NAT st n = (5 * k) + 3 by A4;

hence contradiction by A13, NAT_1:18; :: thesis: verum

A16: now :: thesis: not n in N

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;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

now :: thesis: not n in K

hence
ex r being Element of REAL st Sassume
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;then ex k being Element of NAT st n = (5 * k) + 2 by A3;

hence contradiction by A13, NAT_1:18; :: thesis: verum

suppose A18:
n = (5 * m) + 2
; :: thesis: ex r, r being Element of REAL st S_{6}[n,r]

_{3}(((n - 2) / 5)); :: thesis: ex r being Element of REAL st S_{6}[n,r]

_{6}[n,r]
by A21, A20, A19; :: thesis: verum

end;

A19: now :: thesis: not n in O

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;then ex k being Element of NAT st n = (5 * k) + 4 by A5;

hence contradiction by A18, NAT_1:18; :: thesis: verum

A20: now :: thesis: not n in L

take r = Fassume
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;then ex k being Element of NAT st n = (5 * k) + 3 by A4;

hence contradiction by A18, NAT_1:18; :: thesis: verum

A21: now :: thesis: not n in N

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;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

now :: thesis: not n in M

hence
ex r being Element of REAL st Sassume
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;then ex k being Element of NAT st n = (5 * k) + 1 by A2;

hence contradiction by A18, NAT_1:18; :: thesis: verum

suppose A23:
n = (5 * m) + 3
; :: thesis: ex r, r being Element of REAL st S_{6}[n,r]

_{4}(((n - 3) / 5)); :: thesis: ex r being Element of REAL st S_{6}[n,r]

_{6}[n,r]
by A26, A25, A24; :: thesis: verum

end;

A24: now :: thesis: not n in O

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;then ex k being Element of NAT st n = (5 * k) + 4 by A5;

hence contradiction by A23, NAT_1:18; :: thesis: verum

A25: now :: thesis: not n in K

take r = Fassume
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;then ex k being Element of NAT st n = (5 * k) + 2 by A3;

hence contradiction by A23, NAT_1:18; :: thesis: verum

A26: now :: thesis: not n in N

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;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

now :: thesis: not n in M

hence
ex r being Element of REAL st Sassume
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;then ex k being Element of NAT st n = (5 * k) + 1 by A2;

hence contradiction by A23, NAT_1:18; :: thesis: verum

suppose A28:
n = (5 * m) + 4
; :: thesis: ex r, r being Element of REAL st S_{6}[n,r]

_{5}(((n - 4) / 5)); :: thesis: ex r being Element of REAL st S_{6}[n,r]

_{6}[n,r]
by A31, A30, A29; :: thesis: verum

end;

A29: now :: thesis: not n in L

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;then ex k being Element of NAT st n = (5 * k) + 3 by A4;

hence contradiction by A28, NAT_1:18; :: thesis: verum

A30: now :: thesis: not n in K

take r = Fassume
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;then ex k being Element of NAT st n = (5 * k) + 2 by A3;

hence contradiction by A28, NAT_1:18; :: thesis: verum

A31: now :: thesis: not n in N

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;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

now :: thesis: not n in M

hence
ex r being Element of REAL st Sassume
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;then ex k being Element of NAT st n = (5 * k) + 1 by A2;

hence contradiction by A28, NAT_1:18; :: thesis: verum

A33: for n being Element of NAT holds S

reconsider f = f as Real_Sequence ;

take f ; :: thesis: for n being Element of NAT holds

( f . (5 * n) = F

let n be Element of NAT ; :: thesis: ( f . (5 * n) = F

5 * n in N by A1;

hence f . (5 * n) = F

.= F

:: thesis: ( f . ((5 * n) + 1) = F

(5 * n) + 1 in M by A2;

hence f . ((5 * n) + 1) = F

.= F

:: thesis: ( f . ((5 * n) + 2) = F

(5 * n) + 2 in K by A3;

hence f . ((5 * n) + 2) = F

.= F

:: thesis: ( f . ((5 * n) + 3) = F

(5 * n) + 3 in L by A4;

hence f . ((5 * n) + 3) = F

.= F

:: thesis: f . ((5 * n) + 4) = F

(5 * n) + 4 in O by A5;

hence f . ((5 * n) + 4) = F

.= F

:: thesis: verum