let D be finite set ; :: thesis: for F being one-to-one onto FinSequence of D holds <*F*> is DoubleReorganization of D
let F be one-to-one onto FinSequence of D; :: thesis: <*F*> is DoubleReorganization of D
F is Element of D * by FINSEQ_1:def 11;
then ( {F} c= D * & rng <*F*> = {F} ) by ZFMISC_1:31, FINSEQ_1:38;
then reconsider FF = <*F*> as double-one-to-one FinSequence of D * by FINSEQ_1:def 4;
A1: rngs FF = <*(rng F)*> by FINSEQ_3:132;
rng <*(rng F)*> = {(rng F)} by FINSEQ_1:38;
then union (rng <*(rng F)*>) = rng F by ZFMISC_1:25;
then Union (rngs FF) = rng F by CARD_3:def 4, A1;
then Values FF = rng F by MATRIX_0:def 9;
hence <*F*> is DoubleReorganization of D by FUNCT_2:def 3, Def7; :: thesis: verum