defpred S_{1}[ set ] means ex m being Element of NAT st $1 = 2 * 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 = (2 * 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}[ Element of NAT , set ] means ( ( $1 in N implies $2 = F_{1}(($1 / 2)) ) & ( $1 in M implies $2 = F_{2}((($1 - 1) / 2)) ) );

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

A7: for n being Element of NAT holds S_{3}[n,f . n]
from FUNCT_2:sch 3(A3);

reconsider f = f as Real_Sequence ;

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

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

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

2 * n in N by A1;

hence f . (2 * n) = F_{1}(((2 * n) / 2))
by A7

.= F_{1}(n)
;

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

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

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

.= F_{2}(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

A3: 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_{3}[n,r]

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

end;now :: thesis: ( n in N implies ex r, r being Element of REAL st S_{3}[n,r] )

hence
ex r being Element of REAL st Sassume A4:
n in N
; :: thesis: ex r, r being Element of REAL st S_{3}[n,r]

reconsider r = F_{1}((n / 2)) as Element of REAL ;

take r = r; :: thesis: ex r being Element of REAL st S_{3}[n,r]

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

end;reconsider r = F

take r = r; :: thesis: ex r being Element of REAL st S

now :: thesis: not n in M

hence
ex r being Element of REAL st Sassume
n in M
; :: thesis: contradiction

then A5: ex k being Element of NAT st n = (2 * k) + 1 by A2;

consider m being Element of NAT such that

A6: n = 2 * m by A1, A4;

n = (2 * m) + 0 by A6;

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

end;then A5: ex k being Element of NAT st n = (2 * k) + 1 by A2;

consider m being Element of NAT such that

A6: n = 2 * m by A1, A4;

n = (2 * m) + 0 by A6;

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

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

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

2 * n in N by A1;

hence f . (2 * n) = F

.= F

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

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

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

.= F

:: thesis: verum