let D be non empty finite set ; :: thesis: for A being FinSequence of bool D st len A = card D & A is terms've_same_card_as_number holds
for B being finite set st B = A . (len A) holds
B = D
let A be FinSequence of bool D; :: thesis: ( len A = card D & A is terms've_same_card_as_number implies for B being finite set st B = A . (len A) holds
B = D )
assume A1: ( len A = card D & A is terms've_same_card_as_number ) ; :: thesis: for B being finite set st B = A . (len A) holds
B = D
let B be finite set ; :: thesis: ( B = A . (len A) implies B = D )
assume A2: B = A . (len A) ; :: thesis: B = D
len A <> 0 by A1;
then A4: 0 + 1 <= len A by NAT_1:13;
then A5: card B = card D by A1, A2, Def1;
len A in dom A by A4, FINSEQ_3:27;
then A6: A . (len A) in bool D by FINSEQ_2:13;
assume B <> D ; :: thesis: contradiction
then B c< D by A2, A6, XBOOLE_0:def 8;
hence contradiction by A5, CARD_2:67; :: thesis: verum