let D be non empty finite set ; :: thesis: for a being FinSequence of bool D holds
( a is length_equal_card_of_set iff len a = card D )
let A be FinSequence of bool D; :: thesis: ( A is length_equal_card_of_set iff len A = card D )
thus ( A is length_equal_card_of_set implies len A = card D ) by ZFMISC_1:81; :: thesis: ( len A = card D implies A is length_equal_card_of_set )
assume A1: len A = card D ; :: thesis: A is length_equal_card_of_set
take D ; :: according to REARRAN1:def 3 :: thesis: ( D = union (bool D) & len A = card D )
thus ( D = union (bool D) & len A = card D ) by A1, ZFMISC_1:81; :: thesis: verum