let n be 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 that
A1: 1 <= n and
A2: n <= (len A) - 1 ; :: thesis: (A . (n + 1)) \ (A . n) <> {}
A3: n + 1 <= len A by A2, XREAL_1:19;
n <= n + 1 by NAT_1:11;
then A4: n <= len A by A3, XXREAL_0:2;
then reconsider An1 = A . (n + 1), An = A . n as finite set by A1, A3, Lm2, NAT_1:11;
1 <= n + 1 by NAT_1:11;
then A5: card An1 = n + 1 by A3, Def1;
assume (A . (n + 1)) \ (A . n) = {} ; :: thesis: contradiction
then A6: A . (n + 1) c= A . n by XBOOLE_1:37;
card An = n by A1, A4, Def1;
then n + 1 <= n by A5, A6, NAT_1:43;
then 1 <= n - n by XREAL_1:19;
then 1 <= 0 ;
hence contradiction ; :: thesis: verum