let D be non empty finite set ; :: thesis: for a being FinSequence of bool D holds
( a is lenght_equal_card_of_set iff len a = card D )
let A be FinSequence of bool D; :: thesis: ( A is lenght_equal_card_of_set iff len A = card D )
thus ( A is lenght_equal_card_of_set implies len A = card D ) :: thesis: ( len A = card D implies A is lenght_equal_card_of_set )

proof

assume A is lenght_equal_card_of_set ; :: thesis: len A = card D
then consider B being finite set such that
A1: ( B = union (bool D) & len A = card B ) by Def3;
thus len A = card D by A1, ZFMISC_1:99; :: thesis: verum

end;

assume A2: len A = card D ; :: thesis: A is lenght_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 A2, ZFMISC_1:99; :: thesis: verum