let D be non empty finite set ; :: thesis: for a being terms've_same_card_as_number ascending FinSequence of bool D
for n, m being Nat st n in dom a & m in dom a & n <> m holds
a . n <> a . m
let A be terms've_same_card_as_number ascending FinSequence of bool D; :: thesis: for n, m being Nat st n in dom A & m in dom A & n <> m holds
A . n <> A . m
let n, m be Nat; :: thesis: ( n in dom A & m in dom A & n <> m implies A . n <> A . m )
assume that
A1: n in dom A and
A2: m in dom A and
A3: ( n <> m & A . n = A . m ) ; :: thesis: contradiction
A4: ( 1 <= m & m <= len A ) by A2, FINSEQ_3:25;
A5: ( 1 <= n & n <= len A ) by A1, FINSEQ_3:25;
reconsider Am = A . m as finite set by A4, Lm2;
card Am = m by A4, Def1;
hence contradiction by A3, A5, Def1; :: thesis: verum