let n be Nat; :: thesis: for D being non empty finite set
for a being terms've_same_card_as_number ascending FinSequence of bool D st 1 <= n & n <= (len a) - 1 holds
ex d being Element of D st
( (a . (n + 1)) \ (a . n) = {d} & a . (n + 1) = (a . n) \/ {d} & (a . (n + 1)) \ {d} = a . n )
let D be non empty finite set ; :: thesis: for a being terms've_same_card_as_number ascending FinSequence of bool D st 1 <= n & n <= (len a) - 1 holds
ex d being Element of D st
( (a . (n + 1)) \ (a . n) = {d} & a . (n + 1) = (a . n) \/ {d} & (a . (n + 1)) \ {d} = a . n )
let A be terms've_same_card_as_number ascending FinSequence of bool D; :: thesis: ( 1 <= n & n <= (len A) - 1 implies ex d being Element of D st
( (A . (n + 1)) \ (A . n) = {d} & A . (n + 1) = (A . n) \/ {d} & (A . (n + 1)) \ {d} = A . n ) )
assume that
A1: 1 <= n and
A2: n <= (len A) - 1 ; :: thesis: ex d being Element of D st
( (A . (n + 1)) \ (A . n) = {d} & A . (n + 1) = (A . n) \/ {d} & (A . (n + 1)) \ {d} = A . n )
A3: n + 1 <= len A by A2, XREAL_1:19;
A4: A . n c= A . (n + 1) by A1, A2, Def2;
n <= n + 1 by NAT_1:11;
then A5: 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;
A6: card An = n by A1, A5, Def1;
A7: 1 <= n + 1 by NAT_1:11;
then card An1 = n + 1 by A3, Def1;
then card (An1 \ An) = (n + 1) - n by A4, A6, CARD_2:44
.= 1 ;
then consider x being object such that
A8: {x} = (A . (n + 1)) \ (A . n) by CARD_2:42;
x in (A . (n + 1)) \ (A . n) by A8, ZFMISC_1:31;
then A9: not x in A . n by XBOOLE_0:def 5;
A10: x in A . (n + 1) by A8, ZFMISC_1:31;
n + 1 in dom A by A3, A7, FINSEQ_3:25;
then A . (n + 1) c= D by Lm5;
then reconsider x = x as Element of D by A10;
take x ; :: thesis: ( (A . (n + 1)) \ (A . n) = {x} & A . (n + 1) = (A . n) \/ {x} & (A . (n + 1)) \ {x} = A . n )
thus {x} = (A . (n + 1)) \ (A . n) by A8; :: thesis: ( A . (n + 1) = (A . n) \/ {x} & (A . (n + 1)) \ {x} = A . n )
thus (A . n) \/ {x} = (A . (n + 1)) \/ (A . n) by A8, XBOOLE_1:39
.= A . (n + 1) by A4, XBOOLE_1:12 ; :: thesis: (A . (n + 1)) \ {x} = A . n
hence (A . (n + 1)) \ {x} = ((A . n) \ {x}) \/ ({x} \ {x}) by XBOOLE_1:42
.= ((A . n) \ {x}) \/ {} by XBOOLE_1:37
.= A . n by A9, ZFMISC_1:57 ;
:: thesis: verum