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