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 Element of 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 Element of NAT st n in dom A & m in dom A & n <> m holds
A . n <> A . m
let n, m be Element of NAT ; :: thesis: ( n in dom A & m in dom A & n <> m implies A . n <> A . m )
assume that
A1: ( n in dom A & m in dom A & n <> m ) and
A2: A . n = A . m ; :: thesis: contradiction
A3: ( 1 <= n & n <= len A & 1 <= m & m <= len A ) by A1, FINSEQ_3:27;
then reconsider Am = A . m, An = A . n as finite set by Lm2;
( card Am = m & card An = n ) by A3, Def1;
hence contradiction by A1, A2; :: thesis: verum