deffunc H1( Nat) -> Nat = $1;
let F be FinSequence of REAL ; ex s being Permutation of (dom F) ex n being Element of NAT st
for i being Element of NAT st i in dom F holds
( i in Seg n iff F . (s . i) <> 0 )
defpred S1[ Nat] means F . $1 <> 0 ;
defpred S2[ Nat] means F . $1 = 0 ;
set A = { H1(i) where i is Element of NAT : ( H1(i) in dom F & S1[i] ) } ;
set B = { H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } ;
set N = len F;
A1:
{ H1(i) where i is Element of NAT : ( H1(i) in dom F & S1[i] ) } c= dom F
from FRAENKEL:sch 17();
then A2:
{ H1(i) where i is Element of NAT : ( H1(i) in dom F & S1[i] ) } c= Seg (len F)
by FINSEQ_1:def 3;
reconsider A = { H1(i) where i is Element of NAT : ( H1(i) in dom F & S1[i] ) } as finite set by A1;
A3:
rng (Sgm A) = A
by A2, FINSEQ_1:def 13;
A4:
{ H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } c= dom F
from FRAENKEL:sch 17();
then A5:
{ H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } c= Seg (len F)
by FINSEQ_1:def 3;
reconsider B = { H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } as finite set by A4;
A6:
rng (Sgm B) = B
by A5, FINSEQ_1:def 13;
for x being object holds not x in A /\ B
then
A /\ B = {}
by XBOOLE_0:def 1;
then A9:
A misses B
by XBOOLE_0:def 7;
set s = (Sgm A) ^ (Sgm B);
A10:
Sgm B is one-to-one
by A5, FINSEQ_3:92;
Sgm A is one-to-one
by A2, FINSEQ_3:92;
then A11:
(Sgm A) ^ (Sgm B) is one-to-one
by A3, A6, A9, A10, FINSEQ_3:91;
set n = len (Sgm A);
A12:
len (Sgm A) = card A
by A2, FINSEQ_3:39;
for x being object holds
( x in dom F iff ( x in A or x in B ) )
then A14:
A \/ B = dom F
by XBOOLE_0:def 3;
then A15:
rng ((Sgm A) ^ (Sgm B)) = dom F
by A3, A6, FINSEQ_1:31;
len (Sgm B) = card B
by A5, FINSEQ_3:39;
then len ((Sgm A) ^ (Sgm B)) =
(card A) + (card B)
by A12, FINSEQ_1:22
.=
card (A \/ B)
by A9, CARD_2:40
.=
card (Seg (len F))
by A14, FINSEQ_1:def 3
;
then A16:
len ((Sgm A) ^ (Sgm B)) = len F
by FINSEQ_1:57;
then A17:
dom ((Sgm A) ^ (Sgm B)) = Seg (len F)
by FINSEQ_1:def 3;
A18:
for x being Element of NAT st x in dom F & not x in Seg (len (Sgm A)) holds
ex k being Element of NAT st
( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k )
proof
let x be
Element of
NAT ;
( x in dom F & not x in Seg (len (Sgm A)) implies ex k being Element of NAT st
( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k ) )
assume that A19:
x in dom F
and A20:
not
x in Seg (len (Sgm A))
;
ex k being Element of NAT st
( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k )
A21:
x in Seg (len F)
by A19, FINSEQ_1:def 3;
( not 1
<= x or not
x <= len (Sgm A) )
by A20, FINSEQ_1:1;
then
(len (Sgm A)) + 1
<= x
by A21, FINSEQ_1:1, INT_1:7;
then A22:
((len (Sgm A)) + 1) - (len (Sgm A)) <= x - (len (Sgm A))
by XREAL_1:9;
reconsider k =
x - (len (Sgm A)) as
Element of
NAT by A22, INT_1:3;
take
k
;
( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k )
len ((Sgm A) ^ (Sgm B)) = (len (Sgm A)) + (len (Sgm B))
by FINSEQ_1:22;
then A23:
(len F) - (len (Sgm A)) = len (Sgm B)
by A16;
x <= len F
by A21, FINSEQ_1:1;
then
k <= len (Sgm B)
by A23, XREAL_1:9;
then
k in Seg (len (Sgm B))
by A22, FINSEQ_1:1;
then
k in Seg (card B)
by A5, FINSEQ_3:39;
then A24:
k in dom (Sgm B)
by A5, FINSEQ_3:40;
x = k + (len (Sgm A))
;
hence
(
x = k + (len (Sgm A)) &
k in dom (Sgm B) &
((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k )
by A24, FINSEQ_1:def 7;
verum
end;
dom F = Seg (len F)
by FINSEQ_1:def 3;
then reconsider s = (Sgm A) ^ (Sgm B) as Function of (dom F),(dom F) by A15, A17, FUNCT_2:1;
s is onto
by A15, FUNCT_2:def 3;
then reconsider s = s as Permutation of (dom F) by A11;
take
s
; ex n being Element of NAT st
for i being Element of NAT st i in dom F holds
( i in Seg n iff F . (s . i) <> 0 )
take
len (Sgm A)
; for i being Element of NAT st i in dom F holds
( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 )
let i be Element of NAT ; ( i in dom F implies ( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 ) )
assume A25:
i in dom F
; ( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 )
thus
( i in Seg (len (Sgm A)) implies F . (s . i) <> 0 )
( F . (s . i) <> 0 implies i in Seg (len (Sgm A)) )
thus
( F . (s . i) <> 0 implies i in Seg (len (Sgm A)) )
verum