let D be non empty finite set ; :: thesis: for a being terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool D ex d being Element of D st a . 1 = {d}
let A be terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool D; :: thesis: ex d being Element of D st A . 1 = {d}
len A <> 0 by Th4;
then 0 < len A ;
then A1: 0 + 1 <= len A by NAT_1:13;
then reconsider A1 = A . 1 as finite set by Lm2;
A2: ( card A1 = 1 & 1 in dom A & dom A = dom A ) by A1, Def1, FINSEQ_3:27;
then A3: A . 1 c= D by Lm5;
consider x being set such that
A4: {x} = A . 1 by A2, CARD_2:60;
reconsider x = x as Element of D by A3, A4, ZFMISC_1:37;
take x ; :: thesis: A . 1 = {x}
thus A . 1 = {x} by A4; :: thesis: verum