let D be non empty finite set ; :: thesis: for a being terms've_same_card_as_number length_equal_card_of_set FinSequence of bool D holds a . (len a) = D
let A be terms've_same_card_as_number length_equal_card_of_set FinSequence of bool D; :: thesis: A . (len A) = D
A1: len A = card D by Th1;
then 1 <= len A by NAT_1:14;
then A . (len A) is finite set by Lm2;
hence A . (len A) = D by A1, Lm3; :: thesis: verum