deffunc H_{1}( Nat) -> Nat = $1;

let F be FinSequence of REAL ; :: thesis: 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 S_{1}[ Nat] means F . $1 <> 0 ;

defpred S_{2}[ Nat] means F . $1 = 0 ;

set A = { H_{1}(i) where i is Element of NAT : ( H_{1}(i) in dom F & S_{1}[i] ) } ;

set B = { H_{1}(i) where i is Element of NAT : ( H_{1}(i) in dom F & S_{2}[i] ) } ;

set N = len F;

A1: { H_{1}(i) where i is Element of NAT : ( H_{1}(i) in dom F & S_{1}[i] ) } c= dom F
from FRAENKEL:sch 17();

then A2: { H_{1}(i) where i is Element of NAT : ( H_{1}(i) in dom F & S_{1}[i] ) } c= Seg (len F)
by FINSEQ_1:def 3;

reconsider A = { H_{1}(i) where i is Element of NAT : ( H_{1}(i) in dom F & S_{1}[i] ) } as finite set by A1;

A3: rng (Sgm A) = A by A2, FINSEQ_1:def 13;

A4: { H_{1}(i) where i is Element of NAT : ( H_{1}(i) in dom F & S_{2}[i] ) } c= dom F
from FRAENKEL:sch 17();

then A5: { H_{1}(i) where i is Element of NAT : ( H_{1}(i) in dom F & S_{2}[i] ) } c= Seg (len F)
by FINSEQ_1:def 3;

reconsider B = { H_{1}(i) where i is Element of NAT : ( H_{1}(i) in dom F & S_{2}[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 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 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 )

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 ; :: thesis: 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) ; :: thesis: 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 ; :: thesis: ( i in dom F implies ( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 ) )

assume A25: i in dom F ; :: thesis: ( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 )

thus ( i in Seg (len (Sgm A)) implies F . (s . i) <> 0 ) :: thesis: ( F . (s . i) <> 0 implies i in Seg (len (Sgm A)) )

let F be FinSequence of REAL ; :: thesis: 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 S

defpred S

set A = { H

set B = { H

set N = len F;

A1: { H

then A2: { H

reconsider A = { H

A3: rng (Sgm A) = A by A2, FINSEQ_1:def 13;

A4: { H

then A5: { H

reconsider B = { H

A6: rng (Sgm B) = B by A5, FINSEQ_1:def 13;

for x being object holds not x in A /\ B

proof

then
A /\ B = {}
by XBOOLE_0:def 1;
let x be object ; :: thesis: not x in A /\ B

assume A7: x in A /\ B ; :: thesis: contradiction

then x in B by XBOOLE_0:def 4;

then A8: ex i2 being Element of NAT st

( x = i2 & i2 in dom F & F . i2 = 0 ) ;

x in A by A7, XBOOLE_0:def 4;

then ex i1 being Element of NAT st

( x = i1 & i1 in dom F & F . i1 <> 0 ) ;

hence contradiction by A8; :: thesis: verum

end;assume A7: x in A /\ B ; :: thesis: contradiction

then x in B by XBOOLE_0:def 4;

then A8: ex i2 being Element of NAT st

( x = i2 & i2 in dom F & F . i2 = 0 ) ;

x in A by A7, XBOOLE_0:def 4;

then ex i1 being Element of NAT st

( x = i1 & i1 in dom F & F . i1 <> 0 ) ;

hence contradiction by A8; :: thesis: verum

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 ) )

proof

then A14:
A \/ B = dom F
by XBOOLE_0:def 3;
let x be object ; :: thesis: ( x in dom F iff ( x in A or x in B ) )

thus ( not x in dom F or x in A or x in B ) :: thesis: ( ( x in A or x in B ) implies x in dom F )

end;thus ( not x in dom F or x in A or x in B ) :: thesis: ( ( x in A or x in B ) implies x in dom F )

proof end;

thus
( ( x in A or x in B ) implies x in dom F )
by A1, A4; :: thesis: verumthen 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

dom F = Seg (len F)
by FINSEQ_1:def 3;
let x be Element of NAT ; :: thesis: ( 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)) ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum

end;( 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)) ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum

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 ; :: thesis: 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) ; :: thesis: 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 ; :: thesis: ( i in dom F implies ( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 ) )

assume A25: i in dom F ; :: thesis: ( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 )

thus ( i in Seg (len (Sgm A)) implies F . (s . i) <> 0 ) :: thesis: ( F . (s . i) <> 0 implies i in Seg (len (Sgm A)) )

proof

thus
( F . (s . i) <> 0 implies i in Seg (len (Sgm A)) )
:: thesis: verum
assume
i in Seg (len (Sgm A))
; :: thesis: F . (s . i) <> 0

then A26: i in dom (Sgm A) by FINSEQ_1:def 3;

then s . i = (Sgm A) . i by FINSEQ_1:def 7;

then s . i in A by A3, A26, FUNCT_1:3;

then ex j being Element of NAT st

( s . i = j & j in dom F & F . j <> 0 ) ;

hence F . (s . i) <> 0 ; :: thesis: verum

end;then A26: i in dom (Sgm A) by FINSEQ_1:def 3;

then s . i = (Sgm A) . i by FINSEQ_1:def 7;

then s . i in A by A3, A26, FUNCT_1:3;

then ex j being Element of NAT st

( s . i = j & j in dom F & F . j <> 0 ) ;

hence F . (s . i) <> 0 ; :: thesis: verum

proof

assume A27:
F . (s . i) <> 0
; :: thesis: i in Seg (len (Sgm A))

assume not i in Seg (len (Sgm A)) ; :: thesis: contradiction

then ex k being Element of NAT st

( i = k + (len (Sgm A)) & k in dom (Sgm B) & s . i = (Sgm B) . k ) by A18, A25;

then s . i in rng (Sgm B) by FUNCT_1:3;

then ex j being Element of NAT st

( s . i = j & j in dom F & F . j = 0 ) by A6;

hence contradiction by A27; :: thesis: verum

end;assume not i in Seg (len (Sgm A)) ; :: thesis: contradiction

then ex k being Element of NAT st

( i = k + (len (Sgm A)) & k in dom (Sgm B) & s . i = (Sgm B) . k ) by A18, A25;

then s . i in rng (Sgm B) by FUNCT_1:3;

then ex j being Element of NAT st

( s . i = j & j in dom F & F . j = 0 ) by A6;

hence contradiction by A27; :: thesis: verum