deffunc H1( 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 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 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 ;
A4: { H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } c= dom F from 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 ;
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 ;
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 ;
Sgm A is one-to-one by ;
then A11: (Sgm A) ^ (Sgm B) is one-to-one by ;
set n = len (Sgm A);
A12: len (Sgm A) = card A by ;
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 ;
len (Sgm B) = card B by ;
then len ((Sgm A) ^ (Sgm B)) = (card A) + (card B) by
.= card (A \/ B) by
.= card (Seg (len F)) by ;
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 ;
( not 1 <= x or not x <= len (Sgm A) ) by ;
then (len (Sgm A)) + 1 <= x by ;
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 ;
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 ;
then k <= len (Sgm B) by ;
then k in Seg (len (Sgm B)) by ;
then k in Seg (card B) by ;
then A24: k in dom (Sgm B) by ;
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 ; :: 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 ;
s is onto by ;
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 ;
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 ;
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;