{} = <*> ({} *) ;
then reconsider D = {} as double-one-to-one FinSequence of {} * ;
rngs D = {} --> D by FUNCT_6:23;
then Union (rngs D) = {} by FUNCT_6:26;
then Values D = {} by MATRIX_0:def 9;
hence {} is DoubleReorganization of {} by Def7; :: thesis: <*{}*> is DoubleReorganization of {}
rng {} = {} ;
then reconsider F = {} as FinSequence of {} by FINSEQ_1:def 4;
( {F} c= {} * & rng <*F*> = {F} ) by FINSEQ_1:38;
then reconsider FF = <*F*> as double-one-to-one FinSequence of {} * 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 = {} by MATRIX_0:def 9;
hence <*{}*> is DoubleReorganization of {} by Def7; :: thesis: verum