defpred S1[ set ] means ex m being 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 S1[n] )
from SUBSET_1:sch 3();
defpred S2[ set ] means ex m being 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 S2[n] )
from SUBSET_1:sch 3();
defpred S3[ Nat, set ] means ( ( $1 in N implies $2 = F2(($1 / 2)) ) & ( $1 in M implies $2 = F3((($1 - 1) / 2)) ) );
A3:
for n being Element of NAT ex r being Element of F1() st S3[n,r]
proof
let n be
Element of
NAT ;
ex r being Element of F1() st S3[n,r]
now ( n in N implies ex r being Element of F1() st not n in M )assume A4:
n in N
;
not for r being Element of F1() holds n in Mreconsider r =
F2(
(n / 2)) as
Element of
F1() ;
take r =
r;
not n in Mhereby verum
assume
n in M
;
contradictionthen A5:
ex
k being
Nat st
n = (2 * k) + 1
by A2;
ex
m being
Nat st
n = 2
* m
by A1, A4;
hence
contradiction
by A5;
verum
end; end;
hence
ex
r being
Element of
F1() st
S3[
n,
r]
;
verum
end;
consider f being sequence of F1() such that
A6:
for n being Element of NAT holds S3[n,f . n]
from FUNCT_2:sch 3(A3);
reconsider f = f as sequence of F1() ;
take
f
; for n being Nat holds
( f . (2 * n) = F2(n) & f . ((2 * n) + 1) = F3(n) )
let n be Nat; ( f . (2 * n) = F2(n) & f . ((2 * n) + 1) = F3(n) )
reconsider m = 2 * n as Nat ;
A7:
m in NAT
by ORDINAL1:def 12;
f . ((2 * n) + 1) = F3(((((2 * n) + 1) - 1) / 2))
by A6, A2;
hence
( f . (2 * n) = F2(n) & f . ((2 * n) + 1) = F3(n) )
by A1, A6, A7; verum