let n be Nat; :: thesis: for D being non empty finite set
for a being terms've_same_card_as_number FinSequence of bool D st n in dom a holds
a . n <> {}
let D be non empty finite set ; :: thesis: for a being terms've_same_card_as_number FinSequence of bool D st n in dom a holds
a . n <> {}
let A be terms've_same_card_as_number FinSequence of bool D; :: thesis: ( n in dom A implies A . n <> {} )
assume n in dom A ; :: thesis: A . n <> {}
then A1: ( 1 <= n & n <= len A ) by FINSEQ_3:25;
assume A . n = {} ; :: thesis: contradiction
hence contradiction by A1, Def1, CARD_1:27; :: thesis: verum