deffunc H₁( Nat) -> Element of bool D = D \ (A . ((len A) - $1));
set c = card D;
D c= D ;
then reconsider y = D as Subset of 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;
consider f being FinSequence such that
A1: len f = c1 and
A2: for m being Nat st m in dom f holds
f . m = H₁(m) from FINSEQ_1:sch 2();
A3: dom f = Seg c1 by A1, FINSEQ_1:def 3;
rng f c= bool D

proof

let x be object ; :: 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
A4: ( m in dom f & f . m = x ) by FINSEQ_2:10;
D \ (A . ((len A) - m)) c= D ;
then x is Subset of D by A2, A4;
hence x in bool D ; :: thesis: verum

end;

then reconsider f = f as FinSequence of bool D by FINSEQ_1:def 4;
set C = f ^ <*y*>;
A5: len (f ^ <*y*>) = (len f) + (len <*y*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
A6: card D = len A by Th1;
A7: 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 that
A8: 1 <= m and
A9: m <= len (f ^ <*y*>) ; :: thesis: for B being finite set st B = (f ^ <*y*>) . m holds
card B = m
max (0,((len (f ^ <*y*>)) - m)) = (len (f ^ <*y*>)) - m by A9, 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 A10: B = (f ^ <*y*>) . m ; :: thesis: card B = m

now :: thesis: ( ( m = len (f ^ <*y*>) & card B = m ) or ( m <> len (f ^ <*y*>) & card B = m ) )

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 A1, A5, A10, FINSEQ_1:42; :: thesis: verum

end;

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

then m < len (f ^ <*y*>) by A9, XXREAL_0:1;
then A11: m + 1 <= len (f ^ <*y*>) by NAT_1:13;
then A12: 1 <= l by XREAL_1:19;
A13: l <= len A by A6, A1, A5, XREAL_1:43;
then A14: l in dom A by A12, FINSEQ_3:25;
then reconsider Al = A . l as finite set by Lm5, FINSET_1:1;
m <= (len (f ^ <*y*>)) - 1 by A11, XREAL_1:19;
then A15: m in dom f by A5, A8, FINSEQ_3:25;
then (f ^ <*y*>) . m = f . m by FINSEQ_1:def 7
.= D \ (A . l) by A6, A1, A2, A5, A15 ;
hence card B = (card D) - (card Al) by A10, A14, Lm5, CARD_2:44
.= (len A) - l by A6, A12, A13, Def1
.= m by A6, A1, A5 ;
:: thesis: verum

end;

end;

end;

hence card B = m ; :: thesis: verum

end;

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 that
A16: 1 <= m and
A17: m <= (len (f ^ <*y*>)) - 1 ; :: thesis: (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1)
A18: m in dom f by A5, A16, A17, FINSEQ_3:25;
then A19: (f ^ <*y*>) . m = f . m by FINSEQ_1:def 7
.= D \ (A . ((len A) - m)) by A2, A18 ;

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

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

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

end;

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

then A20: m < (len (f ^ <*y*>)) - 1 by A17, XXREAL_0:1;
then A21: m + 1 < len A by A6, A1, A5, XREAL_1:20;
then max (0,((len A) - (m + 1))) = (len A) - (m + 1) by FINSEQ_2:4;
then reconsider l = (len A) - (m + 1) as Element of NAT by FINSEQ_2:5;
A22: 1 <= m + 1 by NAT_1:11;
m + 1 <= (len (f ^ <*y*>)) - 1 by A5, A20, NAT_1:13;
then A23: m + 1 in dom f by A5, A22, FINSEQ_3:25;
then A24: (f ^ <*y*>) . (m + 1) = f . (m + 1) by FINSEQ_1:def 7
.= D \ (A . l) by A2, A23 ;
(m + 1) + 1 <= len A by A21, NAT_1:13;
then A25: 1 <= (len A) - (m + 1) by XREAL_1:19;
l <= (len A) - 1 by A22, XREAL_1:13;
then A . l c= A . (l + 1) by A25, Def2;
hence (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1) by A19, A24, XBOOLE_1:34; :: thesis: verum

end;

end;

end;

then reconsider C = f ^ <*y*> as RearrangmentGen of D by A1, A5, A7, 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 A26: m in Seg c1 by A1, A5, FINSEQ_1:1;
then m in dom f by A1, FINSEQ_1:def 3;
hence C . m = f . m by FINSEQ_1:def 7
.= D \ (A . ((len A) - m)) by A2, A3, A26 ;
:: thesis: verum