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 that
A1: len A = card D and
A2: A is terms've_same_card_as_number ; :: thesis: for B being finite set st B = A . (len A) holds
B = D
A3: 0 + 1 <= len A by A1, NAT_1:13;
then len A in dom A by FINSEQ_3:25;
then A4: A . (len A) in bool D by FINSEQ_2:11;
let B be finite set ; :: thesis: ( B = A . (len A) implies B = D )
assume A5: B = A . (len A) ; :: thesis: B = D
assume B <> D ; :: thesis: contradiction
then A6: B c< D by A5, A4;
card B = card D by A1, A2, A5, A3;
hence contradiction by A6, CARD_2:48; :: thesis: verum