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 ex d being Element of D st a . 1 = {d}
let A be terms've_same_card_as_number length_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 A1: 0 + 1 <= len A by NAT_1:13;
then reconsider A1 = A . 1 as finite set by Lm2;
card A1 = 1 by A1, Def1;
then consider x being object such that
A2: {x} = A . 1 by CARD_2:42;
1 in dom A by A1, FINSEQ_3:25;
then A . 1 c= D by Lm5;
then reconsider x = x as Element of D by A2, ZFMISC_1:31;
take x ; :: thesis: A . 1 = {x}
thus A . 1 = {x} by A2; :: thesis: verum