consider B being FinSequence of bool D such that
A1:
( len B = card D & B is ascending & B is terms've_same_card_as_number )
by Lm4;
take
B
; ( B is terms've_same_card_as_number & B is ascending & B is length_equal_card_of_set )
union (bool D) = D
by ZFMISC_1:81;
hence
( B is terms've_same_card_as_number & B is ascending & B is length_equal_card_of_set )
by A1; verum