let n be Element of NAT ; :: thesis: for D being non empty finite set
for a being terms've_same_card_as_number FinSequence of bool D st 1 <= n & n <= (len a) - 1 holds
(a . (n + 1)) \ (a . n) <> {}
let D be non empty finite set ; :: thesis: for a being terms've_same_card_as_number FinSequence of bool D st 1 <= n & n <= (len a) - 1 holds
(a . (n + 1)) \ (a . n) <> {}
let A be terms've_same_card_as_number FinSequence of bool D; :: thesis: ( 1 <= n & n <= (len A) - 1 implies (A . (n + 1)) \ (A . n) <> {} )
assume A1: ( 1 <= n & n <= (len A) - 1 ) ; :: thesis: (A . (n + 1)) \ (A . n) <> {}
then A2: ( n + 1 <= len A & n <= n + 1 ) by NAT_1:11, XREAL_1:21;
then A3: ( 1 <= n + 1 & n <= len A ) by A1, XXREAL_0:2;
then reconsider An1 = A . (n + 1), An = A . n as finite set by A1, A2, Lm2;
A4: ( n in dom A & n + 1 in dom A & card An1 = n + 1 & card An = n ) by A1, A2, A3, Def1, FINSEQ_3:27;
assume (A . (n + 1)) \ (A . n) = {} ; :: thesis: contradiction
then A . (n + 1) c= A . n by XBOOLE_1:37;
then n + 1 <= n by A4, NAT_1:44;
then 1 <= n - n by XREAL_1:21;
then 1 <= 0 ;
hence contradiction ; :: thesis: verum