A1: ( card D = len A & A . (len A) = D ) by Th1, Th3;
set c = card D;
0 + 1 <= card D by NAT_1:13;
then max 0 ,((card D) - 1) = (card D) - 1 by FINSEQ_2:4;
then reconsider c1 = (card D) - 1 as Element of NAT by FINSEQ_2:5;
deffunc H₁( Nat) -> Element of bool D = D \ (A . ((len A) - $1));
consider f being FinSequence such that
A2: len f = c1 and
A3: for m being Nat st m in dom f holds
f . m = H₁(m) from FINSEQ_1:sch 2();
A4: dom f = Seg c1 by A2, FINSEQ_1:def 3;
rng f c= bool D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in bool D )
assume x in rng f ; :: thesis: x in bool D
then consider m being Nat such that
A5: ( m in dom f & f . m = x ) by FINSEQ_2:11;
D \ (A . ((len A) - m)) c= D ;
then x is Subset of D by A3, A5;
hence x in bool D ; :: thesis: verum

end;

then reconsider f = f as FinSequence of bool D by FINSEQ_1:def 4;
D c= D ;
then reconsider y = D as Subset of D ;
set C = f ^ <*y*>;
A7: len (f ^ <*y*>) = (len f) + (len <*y*>) by FINSEQ_1:35
.= (len f) + 1 by FINSEQ_1:56 ;
A8: for m being Nat st 1 <= m & m <= (len (f ^ <*y*>)) - 1 holds
(f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1)

proof

let m be Nat; :: thesis: ( 1 <= m & m <= (len (f ^ <*y*>)) - 1 implies (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1) )
assume A9: ( 1 <= m & m <= (len (f ^ <*y*>)) - 1 ) ; :: thesis: (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1)
then A10: m in dom f by A7, FINSEQ_3:27;
then A11: m in Seg (len f) by FINSEQ_1:def 3;
A12: (f ^ <*y*>) . m = f . m by A10, FINSEQ_1:def 7
.= D \ (A . ((len A) - m)) by A2, A3, A11, A4 ;

now

per cases ( m = (len (f ^ <*y*>)) - 1 or m <> (len (f ^ <*y*>)) - 1 ) ;

case m = (len (f ^ <*y*>)) - 1 ; :: thesis: (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1)

then (f ^ <*y*>) . (m + 1) = D by A7, FINSEQ_1:59;
hence (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1) by A12; :: thesis: verum

end;

case m <> (len (f ^ <*y*>)) - 1 ; :: thesis: (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1)

then A13: m < (len (f ^ <*y*>)) - 1 by A9, XXREAL_0:1;
then A14: m + 1 < len A by A1, A2, A7, XREAL_1:22;
then (m + 1) + 1 <= len A by NAT_1:13;
then A15: 1 <= (len A) - (m + 1) by XREAL_1:21;
max 0 ,((len A) - (m + 1)) = (len A) - (m + 1) by A14, FINSEQ_2:4;
then reconsider l = (len A) - (m + 1) as Element of NAT by FINSEQ_2:5;
A16: ( 1 <= m + 1 & m + 1 <= (len (f ^ <*y*>)) - 1 ) by A7, A13, NAT_1:11, NAT_1:13;
then l <= (len A) - 1 by XREAL_1:15;
then A17: ( A . l c= A . (l + 1) & A . l <> A . (l + 1) ) by A15, Def2, Th6;
A18: m + 1 in dom f by A7, A16, FINSEQ_3:27;
then A19: m + 1 in Seg (len f) by FINSEQ_1:def 3;
(f ^ <*y*>) . (m + 1) = f . (m + 1) by A18, FINSEQ_1:def 7
.= D \ (A . l) by A2, A3, A19, A4 ;
hence (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1) by A12, A17, XBOOLE_1:34; :: thesis: verum

end;

end;

end;

hence (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1) ; :: thesis: verum

end;

f ^ <*y*> is terms've_same_card_as_number

proof

let m be Nat; :: according to REARRAN1:def 1 :: thesis: ( 1 <= m & m <= len (f ^ <*y*>) implies for B being finite set st B = (f ^ <*y*>) . m holds
card B = m )
assume A20: ( 1 <= m & m <= len (f ^ <*y*>) ) ; :: thesis: for B being finite set st B = (f ^ <*y*>) . m holds
card B = m
then max 0 ,((len (f ^ <*y*>)) - m) = (len (f ^ <*y*>)) - m by FINSEQ_2:4;
then reconsider l = (len (f ^ <*y*>)) - m as Element of NAT by FINSEQ_2:5;
let B be finite set ; :: thesis: ( B = (f ^ <*y*>) . m implies card B = m )
assume A21: B = (f ^ <*y*>) . m ; :: thesis: card B = m

now

per cases ( m = len (f ^ <*y*>) or m <> len (f ^ <*y*>) ) ;

case m = len (f ^ <*y*>) ; :: thesis: card B = m

hence card B = m by A2, A7, A21, FINSEQ_1:59; :: thesis: verum

end;

case m <> len (f ^ <*y*>) ; :: thesis: card B = m

then m < len (f ^ <*y*>) by A20, XXREAL_0:1;
then m + 1 <= len (f ^ <*y*>) by NAT_1:13;
then A22: ( m <= (len (f ^ <*y*>)) - 1 & 1 <= l ) by XREAL_1:21;
then A23: m in dom f by A7, A20, FINSEQ_3:27;
then A24: m in Seg (len f) by FINSEQ_1:def 3;
A25: (f ^ <*y*>) . m = f . m by A23, FINSEQ_1:def 7
.= D \ (A . l) by A1, A2, A3, A7, A24, A4 ;
A26: l <= len A by A1, A2, A7, XREAL_1:45;
then A27: l in dom A by A22, FINSEQ_3:27;
then reconsider Al = A . l as finite set by Lm5, FINSET_1:13;
thus card B = (card D) - (card Al) by A21, A25, A27, Lm5, CARD_2:63
.= (len A) - l by A1, A22, A26, Def1
.= m by A1, A2, A7 ; :: thesis: verum

end;

end;

end;

hence card B = m ; :: thesis: verum

end;

then reconsider C = f ^ <*y*> as RearrangmentGen of D by A2, A7, A8, Def2, Th1;
take C ; :: thesis: for m being Nat st 1 <= m & m <= (len C) - 1 holds
C . m = D \ (A . ((len A) - m))
let m be Nat; :: thesis: ( 1 <= m & m <= (len C) - 1 implies C . m = D \ (A . ((len A) - m)) )
assume ( 1 <= m & m <= (len C) - 1 ) ; :: thesis: C . m = D \ (A . ((len A) - m))
then A28: m in Seg c1 by A2, A7, FINSEQ_1:3;
then m in dom f by A2, FINSEQ_1:def 3;
hence C . m = f . m by FINSEQ_1:def 7
.= D \ (A . ((len A) - m)) by A3, A28, A4 ;
:: thesis: verum