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

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

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

defpred S_{4}[ Element of NAT , set ] means ( ( $1 in E implies $2 = F_{1}(($1 / 3)) ) & ( $1 in G implies $2 = F_{2}((($1 - 1) / 3)) ) & ( $1 in K implies $2 = F_{3}((($1 - 2) / 3)) ) );

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

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

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

3 * n in E by A1;

hence f . (3 * n) = F_{1}(((3 * n) / 3))
by A15

.= F_{1}(n)
;

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

(3 * n) + 1 in G by A2;

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

.= F_{2}(n)
;

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

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

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

.= F_{3}(n)
;

:: thesis: verum

consider E being Subset of NAT such that

A1: for n being Element of NAT holds

( n in E iff S

defpred S

consider G being Subset of NAT such that

A2: for n being Element of NAT holds

( n in G 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

A4: 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_{4}[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;

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

end;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 S_{4}[n,r]end;

hence
ex r being Element of REAL st Sper cases
( n = 3 * m or n = (3 * m) + 1 or n = (3 * m) + 2 )
by A5;

end;

suppose A6:
n = 3 * m
; :: thesis: ex r, r being Element of REAL st S_{4}[n,r]

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

A7: n = (3 * m) + 0 by A6;

_{4}[n,r]
by A8; :: thesis: verum

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

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

now :: thesis: not n in G

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

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

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

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

_{4}[n,r]
by A10; :: thesis: verum

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

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 = (3 * k) + 2 by A3;

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

end;then ex k being Element of NAT st n = (3 * k) + 2 by A3;

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

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

take r = F_{3}(((n - 2) / 3)); :: thesis: ex r being Element of REAL st S_{4}[n,r]

_{4}[n,r]
by A13; :: thesis: verum

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

now :: thesis: not n in G

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

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

A15: 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 . (3 * n) = F

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

3 * n in E by A1;

hence f . (3 * n) = F

.= F

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

(3 * n) + 1 in G by A2;

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

.= F

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

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

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

.= F

:: thesis: verum