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: len A = card D by Th1;
A2: len (Co_Gen (Co_Gen A)) = card D by Th1;
A3: len (Co_Gen A) = card D by Th1;
A4: 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 A5: m in dom A by FINSEQ_1:def 3;
then A6: m <= len A by FINSEQ_3:25;
A7: 1 <= m by A5, FINSEQ_3:25;

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

( dom A = Seg (len A) & dom (Co_Gen (Co_Gen A)) = Seg (len (Co_Gen (Co_Gen A))) ) by FINSEQ_1:def 3;
hence Co_Gen (Co_Gen A) = A by A1, A2, A4, FINSEQ_1:13; :: thesis: verum