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 ;
deffunc H₁( Nat) -> Nat = $1;
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;
A3: { H₁(i) where i is Element of NAT : ( H₁(i) in dom F & S₂[i] ) } c= dom F from FRAENKEL:sch 17();
then A4: { 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 A3;
A5: ( rng (Sgm A) = A & rng (Sgm B) = B ) by A2, A4, FINSEQ_1:def 13;
for x being set holds not x in A /\ B

proof

let x be set ; :: thesis: not x in A /\ B
assume x in A /\ B ; :: thesis: contradiction
then A6: ( x in A & x in B ) by XBOOLE_0:def 4;
then consider i1 being Element of NAT such that
A7: ( x = i1 & i1 in dom F & F . i1 <> 0 ) ;
consider i2 being Element of NAT such that
A8: ( x = i2 & i2 in dom F & F . i2 = 0 ) by A6;
thus contradiction by A7, A8; :: thesis: verum

end;

then A /\ B = {} by XBOOLE_0:def 1;
then A9: A misses B by XBOOLE_0:def 7;
A10: A \/ B = dom F

proof

for x being set holds
( x in dom F iff ( x in A or x in B ) )

proof

let x be set ; :: 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 A11: 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 A11; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

hence A \/ B = dom F by XBOOLE_0:def 3; :: thesis: verum

end;

set s = (Sgm A) ^ (Sgm B);
A12: len ((Sgm A) ^ (Sgm B)) = len F

proof

( len (Sgm A) = card A & len (Sgm B) = card B ) by A2, A4, FINSEQ_3:44;
then len ((Sgm A) ^ (Sgm B)) = (card A) + (card B) by FINSEQ_1:35
.= card (A \/ B) by A9, CARD_2:53
.= card (Seg (len F)) by A10, FINSEQ_1:def 3 ;
hence len ((Sgm A) ^ (Sgm B)) = len F by FINSEQ_1:78; :: thesis: verum

end;

set n = len (Sgm A);
A13: 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 ( x in dom F & 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 )
then ( x in Seg (len F) & not x in Seg (len (Sgm A)) ) by FINSEQ_1:def 3;
then A14: ( 1 <= x & x <= len F & ( not 1 <= x or not x <= len (Sgm A) ) ) by FINSEQ_1:3;
then (len (Sgm A)) + 1 <= x by INT_1:20;
then A15: ((len (Sgm A)) + 1) - (len (Sgm A)) <= x - (len (Sgm A)) by XREAL_1:11;
then reconsider k = x - (len (Sgm A)) as Element of NAT by INT_1:16;
take k ; :: thesis: ( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k )
A16: x = k + (len (Sgm A)) ;
len ((Sgm A) ^ (Sgm B)) = (len (Sgm A)) + (len (Sgm B)) by FINSEQ_1:35;
then (len F) - (len (Sgm A)) = len (Sgm B) by A12;
then k <= len (Sgm B) by A14, XREAL_1:11;
then k in Seg (len (Sgm B)) by A15, FINSEQ_1:3;
then k in Seg (card B) by A4, FINSEQ_3:44;
then k in dom (Sgm B) by A4, FINSEQ_3:45;
hence ( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k ) by A16, FINSEQ_1:def 7; :: thesis: verum

end;

( Sgm A is one-to-one & Sgm B is one-to-one ) by A2, A4, FINSEQ_3:99;
then A17: (Sgm A) ^ (Sgm B) is one-to-one by A5, A9, FINSEQ_3:98;
A18: rng ((Sgm A) ^ (Sgm B)) = dom F by A5, A10, FINSEQ_1:44;
( dom F = Seg (len F) & dom ((Sgm A) ^ (Sgm B)) = Seg (len F) ) by A12, FINSEQ_1:def 3;
then reconsider s = (Sgm A) ^ (Sgm B) as Function of (dom F),(dom F) by A18, FUNCT_2:3;
s is onto by A18, FUNCT_2:def 3;
then reconsider s = s as Permutation of (dom F) by A17;
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 A19: 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 A20: 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 A5, A20, FUNCT_1:12;
then consider j being Element of NAT such that
A21: ( s . i = j & j in dom F & F . j <> 0 ) ;
thus F . (s . i) <> 0 by A21; :: thesis: verum

end;

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

proof

assume A22: F . (s . i) <> 0 ; :: thesis: i in Seg (len (Sgm A))
assume not i in Seg (len (Sgm A)) ; :: thesis: contradiction
then consider k being Element of NAT such that
A23: ( i = k + (len (Sgm A)) & k in dom (Sgm B) & s . i = (Sgm B) . k ) by A13, A19;
s . i in rng (Sgm B) by A23, FUNCT_1:12;
then consider j being Element of NAT such that
A24: ( s . i = j & j in dom F & F . j = 0 ) by A5;
thus contradiction by A22, A24; :: thesis: verum

end;