let D be non empty finite set ; :: thesis: for A being RearrangmentGen of D holds Co_Gen (Co_Gen A) = A
let A be RearrangmentGen of D; :: thesis: Co_Gen (Co_Gen A) = A
set C = Co_Gen A;
set B = Co_Gen (Co_Gen A);
A1: ( dom A = Seg (len A) & dom (Co_Gen A) = Seg (len (Co_Gen A)) & dom (Co_Gen (Co_Gen A)) = Seg (len (Co_Gen (Co_Gen A))) ) by FINSEQ_1:def 3;
A2: ( len (Co_Gen A) = card D & len A = card D & len (Co_Gen (Co_Gen A)) = card D ) by Th1;
for m being Nat st m in Seg (len A) holds
A . m = (Co_Gen (Co_Gen A)) . m

proof

let m be Nat; :: thesis: ( m in Seg (len A) implies A . m = (Co_Gen (Co_Gen A)) . m )
assume m in Seg (len A) ; :: thesis: A . m = (Co_Gen (Co_Gen A)) . m
then A3: m in dom A by FINSEQ_1:def 3;
then A4: ( 1 <= m & m <= len A ) by FINSEQ_3:27;

now

per cases ( m = len A or m <> len A ) ;

case m = len A ; :: thesis: A . m = (Co_Gen (Co_Gen A)) . m

then ( A . m = D & (Co_Gen (Co_Gen A)) . m = D ) by A2, Th3;
hence A . m = (Co_Gen (Co_Gen A)) . m ; :: thesis: verum

end;

case m <> len A ; :: thesis: (Co_Gen (Co_Gen A)) . m = A . m

then m < len A by A4, XXREAL_0:1;
then A5: m + 1 <= len A by NAT_1:13;
then A6: m <= (len A) - 1 by XREAL_1:21;
A7: 1 <= (len A) - m by A5, XREAL_1:21;
A8: (len A) - m <= (len A) - 1 by A4, XREAL_1:15;
max 0 ,((len A) - m) = (len A) - m by A4, FINSEQ_2:4;
then reconsider k = (len A) - m as Element of NAT by FINSEQ_2:5;
(Co_Gen A) . k = D \ (A . ((len A) - k)) by A2, A7, A8, Def4
.= D \ (A . m) ;
hence (Co_Gen (Co_Gen A)) . m = D \ (D \ (A . m)) by A2, A4, A6, Def4
.= D /\ (A . m) by XBOOLE_1:48
.= A . m by A3, Lm5, XBOOLE_1:28 ;
:: thesis: verum

end;

end;

end;

hence A . m = (Co_Gen (Co_Gen A)) . m ; :: thesis: verum

end;

hence Co_Gen (Co_Gen A) = A by A1, A2, FINSEQ_1:17; :: thesis: verum