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

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

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

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

defpred S_{5}[ Element of NAT , set ] means ( ( $1 in Q implies $2 = F_{1}(($1 / 4)) ) & ( $1 in R implies $2 = F_{2}((($1 - 1) / 4)) ) & ( $1 in P implies $2 = F_{3}((($1 - 2) / 4)) ) & ( $1 in L implies $2 = F_{4}((($1 - 3) / 4)) ) );

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

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

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

4 * n in Q by A1;

hence f . (4 * n) = F_{1}(((4 * n) / 4))
by A23

.= F_{1}(n)
;

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

(4 * n) + 1 in R by A2;

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

.= F_{2}(n)
;

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

(4 * n) + 2 in P by A3;

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

.= F_{3}(n)
;

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

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

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

.= F_{4}(n)
;

:: thesis: verum

consider Q being Subset of NAT such that

A1: for n being Element of NAT holds

( n in Q iff S

defpred S

consider R being Subset of NAT such that

A2: for n being Element of NAT holds

( n in R iff S

defpred S

consider P being Subset of NAT such that

A3: for n being Element of NAT holds

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

A5: 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_{5}[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;

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

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

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

end;

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

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

A8: n = (4 * m) + 0 by A7;

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

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

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

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

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

now :: thesis: not n in R

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

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

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

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

_{5}[n,r]
by A12, A14; :: thesis: verum

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

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

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

now :: thesis: not n in P

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

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

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

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

_{5}[n,r]
by A16, A18; :: thesis: verum

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

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

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

now :: thesis: not n in R

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

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

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

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

_{5}[n,r]
by A20, A22; :: thesis: verum

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

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

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

now :: thesis: not n in R

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

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

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

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

4 * n in Q by A1;

hence f . (4 * n) = F

.= F

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

(4 * n) + 1 in R by A2;

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

.= F

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

(4 * n) + 2 in P by A3;

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

.= F

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

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

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

.= F

:: thesis: verum