let l be Nat; :: thesis: ( ( for p being FinSequence
for A being set st len p = l holds
for n being Nat 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 Nat 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 Nat 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 Nat 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 Nat 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 Nat 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 ) )
reconsider q = p | (Seg l) as FinSequence by FINSEQ_1:15;
assume A2: len p = l + 1 ; :: thesis: for n being Nat 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 )
then A3: len q = l by Th51;
let n be Nat; :: 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 ) )
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 object ; :: 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 ;
assume A4: 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 A5: 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 A6: not p . n in A ; :: thesis: (p - A) . (n - (card C)) = p . n

now :: thesis: (p - A) . (n - (card C)) = p . n

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

A8: n in Seg (l + 1) by A2, A4, FINSEQ_1:def 3;
not n in {(l + 1)} by A6, A7, TARSKI:def 1;
then n in (Seg (l + 1)) \ {(l + 1)} by A8, XBOOLE_0:def 5;
then A9: n in Seg l by FINSEQ_1:10;
A10: B = C

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in C )
A11: dom q c= dom p by RELAT_1:60;
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 ;
p . k in A by A13, A15, FUNCT_1:47;
hence x in C by A5, A12, A13, A14, A11; :: thesis: verum

end;

let x be object ; :: 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
A16: x = m and
A17: m in dom p and
A18: m <= n and
A19: p . m in A by A5;
m in Seg (len p) by A17, FINSEQ_1:def 3;
then A20: 1 <= m by FINSEQ_1:1;
n <= l by A9, FINSEQ_1:1;
then m <= l by A18, XXREAL_0:2;
then m in Seg l by A20, FINSEQ_1:1;
then A21: m in dom q by A3, FINSEQ_1:def 3;
then q . m in A by A19, FUNCT_1:47;
hence x in B by A16, A18, A21; :: thesis: verum

end;

A22: q - A = p - A by A2, A7, Th81;
A23: n in dom q by A3, A9, FINSEQ_1:def 3;
then p . n = q . n by FUNCT_1:47;
hence (p - A) . (n - (card C)) = p . n by A1, A6, A3, A23, A22, A10; :: thesis: verum

end;

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

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

now :: thesis: (p - A) . (n - (card C)) = p . n

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

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

p " A = C

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in p " A or x in C )
assume A26: x in p " A ; :: thesis: x in C
then A27: x in dom p by FUNCT_1:def 7;
then reconsider z = x as Element of NAT ;
A28: p . x in A by A26, FUNCT_1:def 7;
z in Seg n by A2, A25, A27, FINSEQ_1:def 3;
then z <= n by FINSEQ_1:1;
hence x in C by A5, A27, A28; :: thesis: verum

end;

let x be object ; :: 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 A5;
hence x in p " A by FUNCT_1:def 7; :: thesis: verum

end;

then A29: len (p - A) = n - (card C) by A2, A25, Th57;
len <*(p . (l + 1))*> = 1 by FINSEQ_1:39;
then (p - A) . (n - (card C)) = (p - A) . ((len (q - A)) + 1) by A24, A29, FINSEQ_1:22
.= p . (l + 1) by A24, FINSEQ_1:42 ;
hence (p - A) . (n - (card C)) = p . n by A25; :: thesis: verum

end;

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

then A30: not n in {(l + 1)} by TARSKI:def 1;
n in Seg (l + 1) by A2, A4, FINSEQ_1:def 3;
then n in (Seg (l + 1)) \ {(l + 1)} by A30, XBOOLE_0:def 5;
then A31: n in Seg l by FINSEQ_1:10;
then 1 <= n by FINSEQ_1:1;
then n in Seg n by FINSEQ_1:1;
then A32: {n} c= Seg n by ZFMISC_1:31;
A33: (Seg n) \ B c= (Seg l) \ (q " A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Seg n) \ B or x in (Seg l) \ (q " A) )
assume A34: x in (Seg n) \ B ; :: thesis: x in (Seg l) \ (q " A)
then reconsider z = x as Element of NAT ;
A35: x in Seg n by A34, XBOOLE_0:def 5;
then A36: 1 <= z by FINSEQ_1:1;
A37: z <= n by A35, FINSEQ_1:1;

A38: now :: thesis: not z in q " A

assume A39: z in q " A ; :: thesis: contradiction
then A40: z in dom q by FUNCT_1:def 7;
q . z in A by A39, FUNCT_1:def 7;
then z in B by A37, A40;
hence contradiction by A34, XBOOLE_0:def 5; :: thesis: verum

end;

n <= l by A31, FINSEQ_1:1;
then z <= l by A37, XXREAL_0:2;
then z in Seg l by A36, FINSEQ_1:1;
hence x in (Seg l) \ (q " A) by A38, XBOOLE_0:def 5; :: thesis: verum

end;

A41: B = C

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in C )
A42: dom q c= dom p by RELAT_1:60;
assume x in B ; :: thesis: x in C
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 ;
p . k in A by A44, A46, FUNCT_1:47;
hence x in C by A5, A43, A44, A45, A42; :: thesis: verum

end;

let x be object ; :: 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
A47: x = m and
A48: m in dom p and
A49: m <= n and
A50: p . m in A by A5;
m in Seg (len p) by A48, FINSEQ_1:def 3;
then A51: 1 <= m by FINSEQ_1:1;
n <= l by A31, FINSEQ_1:1;
then m <= l by A49, XXREAL_0:2;
then m in Seg l by A51, FINSEQ_1:1;
then A52: m in dom q by A3, FINSEQ_1:def 3;
then q . m in A by A50, FUNCT_1:47;
hence x in B by A47, A49, A52; :: thesis: verum

end;

q " A c= dom q by RELAT_1:132;
then A53: q " A c= Seg l by A3, FINSEQ_1:def 3;
(q " A) \/ ((Seg l) \ (q " A)) = (q " A) \/ (Seg l) by XBOOLE_1:39
.= Seg l by A53, XBOOLE_1:12 ;
then card (Seg l) = (card (q " A)) + (card ((Seg l) \ (q " A))) by CARD_2:40, XBOOLE_1:79;
then A54: len q = (card (q " A)) + (card ((Seg (len q)) \ (q " A))) by A3, FINSEQ_1:57;
set b = card B;
set a = n - (card B);
A55: card (Seg n) = n by FINSEQ_1:57;
A56: n in dom q by A3, A31, FINSEQ_1:def 3;
then A57: not q . n in A by A6, FUNCT_1:47;
A58: B c= (Seg n) \ {n}

proof

let x be object ; :: 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
A59: x = k and
A60: k in dom q and
A61: k <= n and
A62: q . k in A ;
k in Seg (len q) by A60, FINSEQ_1:def 3;
then 1 <= k by FINSEQ_1:1;
then A63: k in Seg n by A61, FINSEQ_1:1;
not k in {n} by A57, A62, TARSKI:def 1;
hence x in (Seg n) \ {n} by A59, A63, XBOOLE_0:def 5; :: thesis: verum

end;

then card B <= card ((Seg n) \ {n}) by NAT_1:43;
then card B <= (card (Seg n)) - (card {n}) by A32, CARD_2:44;
then card B <= (card (Seg n)) - 1 by CARD_1:30;
then card B <= n - 1 by FINSEQ_1:57;
then (card B) + 1 <= n by XREAL_1:19;
then A64: 0 + (card B) < (n - (card B)) + (card B) by NAT_1:13;
then 0 <= n - (card B) by XREAL_1:6;
then reconsider a = n - (card B) as Element of NAT by INT_1:3;
(Seg n) \ {n} c= Seg n by XBOOLE_1:36;
then a = card ((Seg n) \ B) by A58, A55, CARD_2:44, XBOOLE_1:1;
then a <= (len q) - (card (q " A)) by A3, A54, A33, NAT_1:43;
then A65: a <= len (q - A) by Th57;
1 <= a by A64, NAT_1:14;
then a in Seg (len (q - A)) by A65, FINSEQ_1:1;
then A66: a in dom (q - A) by FINSEQ_1:def 3;
p . n = q . n by A56, FUNCT_1:47;
then (q - A) . (n - (card B)) = p . n by A1, A6, A3, A56;
hence (p - A) . (n - (card C)) = p . n by A24, A41, A66, 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