let D be non empty finite set ; :: thesis: for a being terms've_same_card_as_number ascending FinSequence of bool D
for n being Element of NAT st 1 <= n & n <= (len a) - 1 holds
a . n <> a . (n + 1)
let A be terms've_same_card_as_number ascending FinSequence of bool D; :: thesis: for n being Element of NAT st 1 <= n & n <= (len A) - 1 holds
A . n <> A . (n + 1)
let n be Element of NAT ; :: thesis: ( 1 <= n & n <= (len A) - 1 implies A . n <> A . (n + 1) )
assume A1: ( 1 <= n & n <= (len A) - 1 ) ; :: thesis: A . n <> A . (n + 1)
then A2: ( n <= n + 1 & n + 1 <= len A ) by NAT_1:11, XREAL_1:21;
then ( 1 <= n + 1 & n <= len A ) by A1, XXREAL_0:2;
then A3: ( n in dom A & n + 1 in dom A ) by A1, A2, FINSEQ_3:27;
n <> n + 1 ;
hence A . n <> A . (n + 1) by A3, Th5; :: thesis: verum