deffunc H₁( 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₁[ Nat] means F . $1 <> 0 ;
defpred S₂[ Nat] means F . $1 = 0 ;
set A = { H₁(i) where i is Element of NAT : ( H₁(i) in dom F & S₁[i] ) } ;
set B = { H₁(i) where i is Element of NAT : ( H₁(i) in dom F & S₂[i] ) } ;
set N = len F;
A1: { H₁(i) where i is Element of NAT : ( H₁(i) in dom F & S₁[i] ) } c= dom F from FRAENKEL:sch 17();
then A2: { H₁(i) where i is Element of NAT : ( H₁(i) in dom F & S₁[i] ) } c= Seg (len F) by FINSEQ_1:def 3;
reconsider A = { H₁(i) where i is Element of NAT : ( H₁(i) in dom F & S₁[i] ) } as finite set by A1;
a2: A is included_in_Seg by A2, FINSEQ_1:def 13;
then A3: rng (Sgm A) = A by FINSEQ_1:def 14;
A4: { H₁(i) where i is Element of NAT : ( H₁(i) in dom F & S₂[i] ) } c= dom F from FRAENKEL:sch 17();
then A5: { H₁(i) where i is Element of NAT : ( H₁(i) in dom F & S₂[i] ) } c= Seg (len F) by FINSEQ_1:def 3;
reconsider B = { H₁(i) where i is Element of NAT : ( H₁(i) in dom F & S₂[i] ) } as finite set by A4;
a5: B is included_in_Seg by A5, FINSEQ_1:def 13;
then A6: rng (Sgm B) = B by FINSEQ_1:def 14;
for x being object holds not x in A /\ B

proof

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;

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

proof

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 )

proof

assume A13: x in dom F ; :: thesis: ( x in A or x in B )
then reconsider x = x as Element of NAT ;

per cases ( F . x <> 0 or F . x = 0 ) ;

suppose F . x <> 0 ; :: thesis: ( x in A or x in B )

hence ( x in A or x in B ) by A13; :: thesis: verum

end;

suppose F . x = 0 ; :: thesis: ( x in A or x in B )

hence ( x in A or x in B ) by A13; :: thesis: verum

end;

end;

end;

thus ( ( x in A or x in B ) implies x in dom F ) by A1, A4; :: thesis: verum

end;

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

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

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;

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