let n be Element of 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 A1: ( 1 <= n & 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 )
then A2: ( A . n c= A . (n + 1) & n <= n + 1 & n + 1 <= len A ) by Def2, NAT_1:11, XREAL_1:21;
then A3: ( 1 <= n + 1 & n <= len A & dom A = dom A ) by A1, XXREAL_0:2;
then reconsider An1 = A . (n + 1), An = A . n as finite set by A1, A2, Lm2;
A4: ( card An1 = n + 1 & card An = n & n + 1 in dom A & n in dom A ) by A1, A2, A3, Def1, FINSEQ_3:27;
then A5: A . (n + 1) c= D by Lm5;
card (An1 \ An) = (n + 1) - n by A2, A4, CARD_2:63
.= 1 ;
then consider x being set such that
A6: {x} = (A . (n + 1)) \ (A . n) by CARD_2:60;
x in (A . (n + 1)) \ (A . n) by A6, ZFMISC_1:37;
then A7: ( x in A . (n + 1) & not x in A . n ) by XBOOLE_0:def 5;
then reconsider x = x as Element of D by A5;
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 A6; :: thesis: ( A . (n + 1) = (A . n) \/ {x} & (A . (n + 1)) \ {x} = A . n )
thus (A . n) \/ {x} = (A . (n + 1)) \/ (A . n) by A6, XBOOLE_1:39
.= A . (n + 1) by A2, 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 A7, ZFMISC_1:65 ;
:: thesis: verum