let D be non empty finite set ; :: thesis: for a being length_equal_card_of_set FinSequence of bool D holds len a <> 0
let A be length_equal_card_of_set FinSequence of bool D; :: thesis: len A <> 0
assume len A = 0 ; :: thesis: contradiction
then card D = 0 by Th1;
hence contradiction ; :: thesis: verum