let l be natural number ; :: thesis: ( ( for p being FinSequence
for A being set st len p = l holds
for n being natural number st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n ) ) implies for p being FinSequence
for A being set st len p = l + 1 holds
for n being natural number st n in dom p holds
for C being finite set holds
( not C = { m where m is Element of NAT : ( m in dom p & m <= n & p . m in A ) } or p . n in A or (p - A) . (n - (card C)) = p . n ) )
assume A1: for p being FinSequence
for A being set st len p = l holds
for n being natural number st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n ) ; :: thesis: for p being FinSequence
for A being set st len p = l + 1 holds
for n being natural number st n in dom p holds
for C being finite set holds
( not C = { m where m is Element of NAT : ( m in dom p & m <= n & p . m in A ) } or p . n in A or (p - A) . (n - (card C)) = p . n )
let p be FinSequence; :: thesis: for A being set st len p = l + 1 holds
for n being natural number st n in dom p holds
for C being finite set holds
( not C = { m where m is Element of NAT : ( m in dom p & m <= n & p . m in A ) } or p . n in A or (p - A) . (n - (card C)) = p . n )
let A be set ; :: thesis: ( len p = l + 1 implies for n being natural number st n in dom p holds
for C being finite set holds
( not C = { m where m is Element of NAT : ( m in dom p & m <= n & p . m in A ) } or p . n in A or (p - A) . (n - (card C)) = p . n ) )
assume A2: len p = l + 1 ; :: thesis: for n being natural number st n in dom p holds
for C being finite set holds
( not C = { m where m is Element of NAT : ( m in dom p & m <= n & p . m in A ) } or p . n in A or (p - A) . (n - (card C)) = p . n )
let n be natural number ; :: thesis: ( n in dom p implies for C being finite set holds
( not C = { m where m is Element of NAT : ( m in dom p & m <= n & p . m in A ) } or p . n in A or (p - A) . (n - (card C)) = p . n ) )
assume A3: n in dom p ; :: thesis: for C being finite set holds
( not C = { m where m is Element of NAT : ( m in dom p & m <= n & p . m in A ) } or p . n in A or (p - A) . (n - (card C)) = p . n )
let C be finite set ; :: thesis: ( not C = { m where m is Element of NAT : ( m in dom p & m <= n & p . m in A ) } or p . n in A or (p - A) . (n - (card C)) = p . n )
assume A4: C = { m where m is Element of NAT : ( m in dom p & m <= n & p . m in A ) } ; :: thesis: ( p . n in A or (p - A) . (n - (card C)) = p . n )
assume A5: not p . n in A ; :: thesis: (p - A) . (n - (card C)) = p . n
reconsider q = p | (Seg l) as FinSequence by FINSEQ_1:19;
A6: len q = l by A2, Th59;
set B = { k where k is Element of NAT : ( k in dom q & k <= n & q . k in A ) } ;
{ k where k is Element of NAT : ( k in dom q & k <= n & q . k in A ) } c= dom q

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( k in dom q & k <= n & q . k in A ) } or x in dom q )
assume x in { k where k is Element of NAT : ( k in dom q & k <= n & q . k in A ) } ; :: thesis: x in dom q
then ex k being Element of NAT st
( x = k & k in dom q & k <= n & q . k in A ) ;
hence x in dom q ; :: thesis: verum

end;

then reconsider B = { k where k is Element of NAT : ( k in dom q & k <= n & q . k in A ) } as finite set ;

now

per cases ( p . (l + 1) in A or not p . (l + 1) in A ) ;

suppose A7: p . (l + 1) in A ; :: thesis: (p - A) . (n - (card C)) = p . n

then ( not n in {(l + 1)} & n in Seg (l + 1) ) by A2, A3, A5, FINSEQ_1:def 3, TARSKI:def 1;
then n in (Seg (l + 1)) \ {(l + 1)} by XBOOLE_0:def 5;
then A8: n in Seg l by FINSEQ_1:12;
then A9: n in dom q by A6, FINSEQ_1:def 3;
then A10: p . n = q . n by FUNCT_1:70;
A11: q - A = p - A by A2, A7, Th90;
B = C

proof

thus B c= C :: according to XBOOLE_0:def 10 :: thesis: C c= B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in C )
assume x in B ; :: thesis: x in C
then consider k being Element of NAT such that
A12: x = k and
A13: k in dom q and
A14: k <= n and
A15: q . k in A ;
A16: p . k in A by A13, A15, FUNCT_1:70;
dom q c= dom p by RELAT_1:89;
hence x in C by A4, A12, A13, A14, A16; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in B )
assume x in C ; :: thesis: x in B
then consider m being Element of NAT such that
A17: x = m and
A18: m in dom p and
A19: m <= n and
A20: p . m in A by A4;
m in Seg (len p) by A18, FINSEQ_1:def 3;
then ( 1 <= m & n <= l ) by A8, FINSEQ_1:3;
then ( 1 <= m & m <= l ) by A19, XXREAL_0:2;
then m in Seg l by FINSEQ_1:3;
then A21: m in dom q by A6, FINSEQ_1:def 3;
then q . m in A by A20, FUNCT_1:70;
hence x in B by A17, A19, A21; :: thesis: verum

end;

hence (p - A) . (n - (card C)) = p . n by A1, A5, A6, A9, A10, A11; :: thesis: verum

end;

suppose not p . (l + 1) in A ; :: thesis: (p - A) . (n - (card C)) = p . n

then A22: p - A = (q - A) ^ <*(p . (l + 1))*> by A2, Th91;

now

per cases ( n = l + 1 or n <> l + 1 ) ;

suppose A23: n = l + 1 ; :: thesis: (p - A) . (n - (card C)) = p . n

A24: len <*(p . (l + 1))*> = 1 by FINSEQ_1:56;
p " A = C

proof

thus p " A c= C :: according to XBOOLE_0:def 10 :: thesis: C c= p " A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in p " A or x in C )
assume x in p " A ; :: thesis: x in C
then A25: ( x in dom p & p . x in A ) by FUNCT_1:def 13;
then reconsider z = x as Element of NAT ;
z in Seg n by A2, A23, A25, FINSEQ_1:def 3;
then z <= n by FINSEQ_1:3;
hence x in C by A4, A25; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in p " A )
assume x in C ; :: thesis: x in p " A
then ex m being Element of NAT st
( x = m & m in dom p & m <= n & p . m in A ) by A4;
hence x in p " A by FUNCT_1:def 13; :: thesis: verum

end;

then len (p - A) = n - (card C) by A2, A23, Th66;
then (p - A) . (n - (card C)) = (p - A) . ((len (q - A)) + 1) by A22, A24, FINSEQ_1:35
.= p . (l + 1) by A22, FINSEQ_1:59 ;
hence (p - A) . (n - (card C)) = p . n by A23; :: thesis: verum

end;

suppose n <> l + 1 ; :: thesis: (p - A) . (n - (card C)) = p . n

then ( not n in {(l + 1)} & n in Seg (l + 1) ) by A2, A3, FINSEQ_1:def 3, TARSKI:def 1;
then n in (Seg (l + 1)) \ {(l + 1)} by XBOOLE_0:def 5;
then A26: n in Seg l by FINSEQ_1:12;
then A27: n in dom q by A6, FINSEQ_1:def 3;
then A28: p . n = q . n by FUNCT_1:70;
A29: not q . n in A by A5, A27, FUNCT_1:70;
A30: (q - A) . (n - (card B)) = p . n by A1, A5, A6, A27, A28;
A31: B = C

proof

thus B c= C :: according to XBOOLE_0:def 10 :: thesis: C c= B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in C )
assume x in B ; :: thesis: x in C
then consider k being Element of NAT such that
A32: x = k and
A33: k in dom q and
A34: k <= n and
A35: q . k in A ;
A36: p . k in A by A33, A35, FUNCT_1:70;
dom q c= dom p by RELAT_1:89;
hence x in C by A4, A32, A33, A34, A36; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in B )
assume x in C ; :: thesis: x in B
then consider m being Element of NAT such that
A37: x = m and
A38: m in dom p and
A39: m <= n and
A40: p . m in A by A4;
m in Seg (len p) by A38, FINSEQ_1:def 3;
then ( 1 <= m & n <= l ) by A26, FINSEQ_1:3;
then ( 1 <= m & m <= l ) by A39, XXREAL_0:2;
then m in Seg l by FINSEQ_1:3;
then A41: m in dom q by A6, FINSEQ_1:def 3;
then q . m in A by A40, FUNCT_1:70;
hence x in B by A37, A39, A41; :: thesis: verum

end;

set a = n - (card B);
set b = card B;
A42: B c= (Seg n) \ {n}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in (Seg n) \ {n} )
assume x in B ; :: thesis: x in (Seg n) \ {n}
then consider k being Element of NAT such that
A43: x = k and
A44: k in dom q and
A45: k <= n and
A46: q . k in A ;
k in Seg (len q) by A44, FINSEQ_1:def 3;
then 1 <= k by FINSEQ_1:3;
then A47: k in Seg n by A45, FINSEQ_1:3;
not k in {n} by A29, A46, TARSKI:def 1;
hence x in (Seg n) \ {n} by A43, A47, XBOOLE_0:def 5; :: thesis: verum

end;

( 1 <= n & n <= n ) by A26, FINSEQ_1:3;
then n in Seg n by FINSEQ_1:3;
then A48: {n} c= Seg n by ZFMISC_1:37;
card B <= card ((Seg n) \ {n}) by A42, NAT_1:44;
then card B <= (card (Seg n)) - (card {n}) by A48, CARD_2:63;
then card B <= (card (Seg n)) - 1 by CARD_1:50;
then card B <= n - 1 by FINSEQ_1:78;
then (card B) + 1 <= n by XREAL_1:21;
then A49: 0 + (card B) < (n - (card B)) + (card B) by NAT_1:13;
then 0 <= n - (card B) by XREAL_1:8;
then reconsider a = n - (card B) as Element of NAT by INT_1:16;
A50: 1 <= a by A49, NAT_1:14;
q " A c= dom q by RELAT_1:167;
then A51: q " A c= Seg l by A6, FINSEQ_1:def 3;
(q " A) \/ ((Seg l) \ (q " A)) = (q " A) \/ (Seg l) by XBOOLE_1:39
.= Seg l by A51, XBOOLE_1:12 ;
then card (Seg l) = (card (q " A)) + (card ((Seg l) \ (q " A))) by CARD_2:53, XBOOLE_1:79;
then A52: len q = (card (q " A)) + (card ((Seg (len q)) \ (q " A))) by A6, FINSEQ_1:78;
(Seg n) \ {n} c= Seg n by XBOOLE_1:36;
then ( B c= Seg n & card (Seg n) = n ) by A42, FINSEQ_1:78, XBOOLE_1:1;
then A53: a = card ((Seg n) \ B) by CARD_2:63;
(Seg n) \ B c= (Seg l) \ (q " A)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Seg n) \ B or x in (Seg l) \ (q " A) )
assume A54: x in (Seg n) \ B ; :: thesis: x in (Seg l) \ (q " A)
then A55: x in Seg n by XBOOLE_0:def 5;
reconsider z = x as Element of NAT by A54;
A56: ( z <= n & n <= l ) by A26, A55, FINSEQ_1:3;
then ( 1 <= z & z <= l ) by A55, FINSEQ_1:3, XXREAL_0:2;
then A57: z in Seg l by FINSEQ_1:3;

now

assume z in q " A ; :: thesis: contradiction
then ( q . z in A & z in dom q ) by FUNCT_1:def 13;
then ( z in B & not z in B ) by A54, A56, XBOOLE_0:def 5;
hence contradiction ; :: thesis: verum

end;

hence x in (Seg l) \ (q " A) by A57, XBOOLE_0:def 5; :: thesis: verum

end;

then a <= (len q) - (card (q " A)) by A6, A52, A53, NAT_1:44;
then a <= len (q - A) by Th66;
then a in Seg (len (q - A)) by A50, FINSEQ_1:3;
then a in dom (q - A) by FINSEQ_1:def 3;
hence (p - A) . (n - (card C)) = p . n by A22, A30, A31, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

hence (p - A) . (n - (card C)) = p . n ; :: thesis: verum

end;

end;

end;

hence (p - A) . (n - (card C)) = p . n ; :: thesis: verum