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 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 Nat st 1 <= n & n <= (len A) - 1 holds
A . n <> A . (n + 1)
let n be Nat; :: thesis: ( 1 <= n & n <= (len A) - 1 implies A . n <> A . (n + 1) )
assume that
A1: 1 <= n and
A2: n <= (len A) - 1 ; :: thesis: A . n <> A . (n + 1)
A3: n + 1 <= len A by A2, XREAL_1:19;
n <= n + 1 by NAT_1:11;
then n <= len A by A3, XXREAL_0:2;
then A4: n in dom A by A1, FINSEQ_3:25;
1 <= n + 1 by NAT_1:11;
then A5: n + 1 in dom A by A3, FINSEQ_3:25;
n <> n + 1 ;
hence A . n <> A . (n + 1) by A4, A5, Th5; :: thesis: verum