let p be FinSequence; :: thesis: for x being object
for A being set holds (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)
let x be object ; :: thesis: for A being set holds (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)
let A be set ; :: thesis: (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)
set r = (p ^ <*x*>) - A;
set q = <*x*> - A;
set t = p ^ <*x*>;
A1: len (p ^ <*x*>) = (len p) + (len <*x*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
A2: now :: thesis: for k being Nat st k in dom (<*x*> - A) holds
((p ^ <*x*>) - A) . ((len (p - A)) + k) = (<*x*> - A) . k
(p ^ <*x*>) " A c= dom (p ^ <*x*>) by RELAT_1:132;
then A3: (p ^ <*x*>) " A c= Seg (len (p ^ <*x*>)) by FINSEQ_1:def 3;
set S = (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A);
set s = Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A));
let k be Nat; :: thesis: ( k in dom (<*x*> - A) implies ((p ^ <*x*>) - A) . ((len (p - A)) + k) = (<*x*> - A) . k )
A4: (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) c= Seg (len (p ^ <*x*>)) by XBOOLE_1:36;
assume A5: k in dom (<*x*> - A) ; :: thesis: ((p ^ <*x*>) - A) . ((len (p - A)) + k) = (<*x*> - A) . k
then A6: not x in A by Lm7, RELAT_1:38;
then A7: <*x*> - A = <*x*> by Lm6;
then A8: dom (<*x*> - A) = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then A9: k = 1 by A5, TARSKI:def 1;
A10: p " A = (p ^ <*x*>) " A
proof
thus p " A c= (p ^ <*x*>) " A :: according to XBOOLE_0:def 10 :: thesis: (p ^ <*x*>) " A c= p " A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in p " A or y in (p ^ <*x*>) " A )
assume A11: y in p " A ; :: thesis: y in (p ^ <*x*>) " A
then A12: y in dom p by FUNCT_1:def 7;
then reconsider z = y as Element of NAT ;
p . y in A by A11, FUNCT_1:def 7;
then A13: (p ^ <*x*>) . z in A by A12, FINSEQ_1:def 7;
y in dom (p ^ <*x*>) by A12, Th22;
hence y in (p ^ <*x*>) " A by A13, FUNCT_1:def 7; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (p ^ <*x*>) " A or y in p " A )
assume A14: y in (p ^ <*x*>) " A ; :: thesis: y in p " A
then A15: y in dom (p ^ <*x*>) by FUNCT_1:def 7;
then reconsider z = y as Element of NAT ;
A16: (p ^ <*x*>) . y in A by A14, FUNCT_1:def 7;
A17: now :: thesis: for n being Nat holds
( not n in dom (<*x*> - A) or not z = (len p) + n )
given n being Nat such that A18: n in dom (<*x*> - A) and
A19: z = (len p) + n ; :: thesis: contradiction
n = 1 by A8, A18, TARSKI:def 1;
hence contradiction by A6, A16, A19, FINSEQ_1:42; :: thesis: verum
end;
A20: ( z in dom p or ex n being Nat st
( n in dom (<*x*> - A) & z = (len p) + n ) ) by A7, A15, FINSEQ_1:25;
then (p ^ <*x*>) . z = p . z by A17, FINSEQ_1:def 7;
hence y in p " A by A16, A20, A17, FUNCT_1:def 7; :: thesis: verum
end;
A21: now :: thesis: not len (p ^ <*x*>) in (p ^ <*x*>) " A
assume A22: len (p ^ <*x*>) in (p ^ <*x*>) " A ; :: thesis: contradiction
(p ^ <*x*>) . (len (p ^ <*x*>)) = x by A1, FINSEQ_1:42;
hence contradiction by A6, A22, FUNCT_1:def 7; :: thesis: verum
end;
A23: dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = Seg (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))) by FINSEQ_1:def 3;
len (p ^ <*x*>) in Seg (len (p ^ <*x*>)) by A1, FINSEQ_1:4;
then len (p ^ <*x*>) in (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) by A21, XBOOLE_0:def 5;
then len (p ^ <*x*>) in rng (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by A4, FINSEQ_1:def 13;
then consider y being object such that
A24: y in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) and
A25: (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . y = len (p ^ <*x*>) by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A24;
A26: (len (p - A)) + k = ((len p) - (card (p " A))) + k by Th57
.= ((len p) + 1) - (card ((p ^ <*x*>) " A)) by A9, A10
.= ((len p) + (len <*x*>)) - (card ((p ^ <*x*>) " A)) by FINSEQ_1:39
.= (len (p ^ <*x*>)) - (card ((p ^ <*x*>) " A)) by FINSEQ_1:22
.= len ((p ^ <*x*>) - A) by Th57 ;
A27: len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = card ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)) by Th37, XBOOLE_1:36
.= (card (Seg (len (p ^ <*x*>)))) - (card ((p ^ <*x*>) " A)) by A3, CARD_2:44
.= (len (p ^ <*x*>)) - (card (p " A)) by A10, FINSEQ_1:57
.= ((len p) - (card (p " A))) + k by A1, A9
.= len ((p ^ <*x*>) - A) by A26, Th57 ;
then A28: len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = (len (p - A)) + 1 by A5, A8, A26, TARSKI:def 1;
then A29: len ((p ^ <*x*>) - A) in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by A27, A23, FINSEQ_1:4;
A30: now :: thesis: not y <> len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
A31: (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))) in rng (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by A27, A29, FUNCT_1:def 3;
reconsider w = (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))) as Element of NAT by A31;
w in (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) by A4, A31, FINSEQ_1:def 13;
then A32: w in Seg (len (p ^ <*x*>)) by XBOOLE_0:def 5;
assume A33: y <> len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) ; :: thesis: contradiction
A34: y in Seg (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))) by A24, FINSEQ_1:def 3;
then y <= len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by FINSEQ_1:1;
then A35: y < len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by A33, XXREAL_0:1;
1 <= y by A34, FINSEQ_1:1;
then len (p ^ <*x*>) < w by A4, A25, A35, FINSEQ_1:def 13;
hence contradiction by A32, FINSEQ_1:1; :: thesis: verum
end;
dom (p ^ <*x*>) = Seg (len (p ^ <*x*>)) by FINSEQ_1:def 3;
hence ((p ^ <*x*>) - A) . ((len (p - A)) + k) = (p ^ <*x*>) . (len (p ^ <*x*>)) by A26, A27, A28, A23, A25, A30, FINSEQ_1:4, FUNCT_1:13
.= x by A1, FINSEQ_1:42
.= (<*x*> - A) . k by A7, A9, FINSEQ_1:def 8 ;
:: thesis: verum
end;
A36: now :: thesis: for k being Nat st k in dom (p - A) holds
((p ^ <*x*>) - A) . k = (p - A) . k
A37: ( x in A implies (p ^ <*x*>) " A = (p " A) \/ {((len p) + 1)} )
proof
assume A38: x in A ; :: thesis: (p ^ <*x*>) " A = (p " A) \/ {((len p) + 1)}
thus (p ^ <*x*>) " A c= (p " A) \/ {((len p) + 1)} :: according to XBOOLE_0:def 10 :: thesis: (p " A) \/ {((len p) + 1)} c= (p ^ <*x*>) " A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (p ^ <*x*>) " A or y in (p " A) \/ {((len p) + 1)} )
assume A39: y in (p ^ <*x*>) " A ; :: thesis: y in (p " A) \/ {((len p) + 1)}
then y in dom (p ^ <*x*>) by FUNCT_1:def 7;
then y in Seg ((len p) + 1) by A1, FINSEQ_1:def 3;
then A40: y in (Seg (len p)) \/ {((len p) + 1)} by FINSEQ_1:9;
now :: thesis: y in (p " A) \/ {((len p) + 1)}
per cases ( y in Seg (len p) or y in {((len p) + 1)} ) by A40, XBOOLE_0:def 3;
suppose A41: y in Seg (len p) ; :: thesis: y in (p " A) \/ {((len p) + 1)}
then reconsider j = y as Element of NAT ;
A42: (p ^ <*x*>) . y in A by A39, FUNCT_1:def 7;
A43: y in dom p by A41, FINSEQ_1:def 3;
then p . j = (p ^ <*x*>) . j by FINSEQ_1:def 7;
then y in p " A by A43, A42, FUNCT_1:def 7;
hence y in (p " A) \/ {((len p) + 1)} by XBOOLE_0:def 3; :: thesis: verum
end;
suppose y in {((len p) + 1)} ; :: thesis: y in (p " A) \/ {((len p) + 1)}
hence y in (p " A) \/ {((len p) + 1)} by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence y in (p " A) \/ {((len p) + 1)} ; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (p " A) \/ {((len p) + 1)} or y in (p ^ <*x*>) " A )
assume A44: y in (p " A) \/ {((len p) + 1)} ; :: thesis: y in (p ^ <*x*>) " A
now :: thesis: y in (p ^ <*x*>) " A
per cases ( y in p " A or y in {((len p) + 1)} ) by A44, XBOOLE_0:def 3;
suppose A45: y in p " A ; :: thesis: y in (p ^ <*x*>) " A
p " A c= (p ^ <*x*>) " A by Th56;
hence y in (p ^ <*x*>) " A by A45; :: thesis: verum
end;
end;
end;
hence y in (p ^ <*x*>) " A ; :: thesis: verum
end;
(p ^ <*x*>) " A c= dom (p ^ <*x*>) by RELAT_1:132;
then A48: (p ^ <*x*>) " A c= Seg (len (p ^ <*x*>)) by FINSEQ_1:def 3;
A49: ( not x in A implies (p ^ <*x*>) " A = p " A )
proof
assume A50: not x in A ; :: thesis: (p ^ <*x*>) " A = p " A
thus (p ^ <*x*>) " A c= p " A :: according to XBOOLE_0:def 10 :: thesis: p " A c= (p ^ <*x*>) " A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (p ^ <*x*>) " A or y in p " A )
assume A51: y in (p ^ <*x*>) " A ; :: thesis: y in p " A
then A52: y in dom (p ^ <*x*>) by FUNCT_1:def 7;
then reconsider l = y as Element of NAT ;
A53: now :: thesis: not l = (len p) + 1
assume l = (len p) + 1 ; :: thesis: contradiction
then (p ^ <*x*>) . l = x by FINSEQ_1:42;
hence contradiction by A50, A51, FUNCT_1:def 7; :: thesis: verum
end;
A54: y in Seg (len (p ^ <*x*>)) by A52, FINSEQ_1:def 3;
then l <= (len p) + 1 by A1, FINSEQ_1:1;
then l < (len p) + 1 by A53, XXREAL_0:1;
then A55: l <= len p by NAT_1:13;
1 <= l by A54, FINSEQ_1:1;
then l in Seg (len p) by A55, FINSEQ_1:1;
then A56: y in dom p by FINSEQ_1:def 3;
(p ^ <*x*>) . l in A by A51, FUNCT_1:def 7;
then p . l in A by A56, FINSEQ_1:def 7;
hence y in p " A by A56, FUNCT_1:def 7; :: thesis: verum
end;
thus p " A c= (p ^ <*x*>) " A by Th56; :: thesis: verum
end;
set s2 = Sgm ((Seg (len p)) \ (p " A));
set s1 = Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A));
let k be Nat; :: thesis: ( k in dom (p - A) implies ((p ^ <*x*>) - A) . k = (p - A) . k )
A57: dom p = Seg (len p) by FINSEQ_1:def 3;
A58: now :: thesis: ( (p ^ <*x*>) " A = p " A implies (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) = ((Seg (len p)) \ (p " A)) \/ {((len p) + 1)} )
{((len p) + 1)} /\ (p " A) = {}
proof
set z = the Element of {((len p) + 1)} /\ (p " A);
A59: p " A c= dom p by RELAT_1:132;
assume A60: not {((len p) + 1)} /\ (p " A) = {} ; :: thesis: contradiction
then the Element of {((len p) + 1)} /\ (p " A) in {((len p) + 1)} by XBOOLE_0:def 4;
then A61: the Element of {((len p) + 1)} /\ (p " A) = (len p) + 1 by TARSKI:def 1;
A62: dom p = Seg (len p) by FINSEQ_1:def 3;
the Element of {((len p) + 1)} /\ (p " A) in p " A by A60, XBOOLE_0:def 4;
then (len p) + 1 <= len p by A61, A59, A62, FINSEQ_1:1;
hence contradiction by XREAL_1:29; :: thesis: verum
end;
then A63: {((len p) + 1)} misses p " A ;
assume (p ^ <*x*>) " A = p " A ; :: thesis: (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) = ((Seg (len p)) \ (p " A)) \/ {((len p) + 1)}
hence (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) = ((Seg (len p)) \/ {((len p) + 1)}) \ (p " A) by A1, FINSEQ_1:9
.= ((Seg (len p)) \ (p " A)) \/ ({((len p) + 1)} \ (p " A)) by XBOOLE_1:42
.= ((Seg (len p)) \ (p " A)) \/ {((len p) + 1)} by A63, XBOOLE_1:83 ;
:: thesis: verum
end;
(Seg (len p)) /\ {((len p) + 1)} = {}
proof
set z = the Element of (Seg (len p)) /\ {((len p) + 1)};
assume A64: not (Seg (len p)) /\ {((len p) + 1)} = {} ; :: thesis: contradiction
then A65: the Element of (Seg (len p)) /\ {((len p) + 1)} in Seg (len p) by XBOOLE_0:def 4;
then reconsider f = the Element of (Seg (len p)) /\ {((len p) + 1)} as Element of NAT ;
f in {((len p) + 1)} by A64, XBOOLE_0:def 4;
then A66: f = (len p) + 1 by TARSKI:def 1;
f <= len p by A65, FINSEQ_1:1;
hence contradiction by A66, XREAL_1:29; :: thesis: verum
end;
then A67: Seg (len p) misses {((len p) + 1)} ;
A68: now :: thesis: ( (p ^ <*x*>) " A = (p " A) \/ {((len p) + 1)} implies (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) = (Seg (len p)) \ (p " A) )
assume (p ^ <*x*>) " A = (p " A) \/ {((len p) + 1)} ; :: thesis: (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) = (Seg (len p)) \ (p " A)
hence (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) = ((Seg (len p)) \/ {((len p) + 1)}) \ ((p " A) \/ {((len p) + 1)}) by A1, FINSEQ_1:9
.= ((Seg (len p)) \ ((p " A) \/ {((len p) + 1)})) \/ ({((len p) + 1)} \ ((p " A) \/ {((len p) + 1)})) by XBOOLE_1:42
.= ((Seg (len p)) \ ((p " A) \/ {((len p) + 1)})) \/ {} by XBOOLE_1:46
.= ((Seg (len p)) \ (p " A)) /\ ((Seg (len p)) \ {((len p) + 1)}) by XBOOLE_1:53
.= ((Seg (len p)) \ (p " A)) /\ (Seg (len p)) by A67, XBOOLE_1:83
.= (Seg (len p)) \ (p " A) by XBOOLE_1:28, XBOOLE_1:36 ;
:: thesis: verum
end;
p " A c= dom p by RELAT_1:132;
then A69: p " A c= Seg (len p) by FINSEQ_1:def 3;
len (Sgm ((Seg (len p)) \ (p " A))) = card ((Seg (len p)) \ (p " A)) by Th37, XBOOLE_1:36
.= (card (Seg (len p))) - (card (p " A)) by A69, CARD_2:44 ;
then A70: len (Sgm ((Seg (len p)) \ (p " A))) = (len p) - (card (p " A)) by FINSEQ_1:57;
(Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) c= Seg (len (p ^ <*x*>)) by XBOOLE_1:36;
then A71: rng (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) c= Seg (len (p ^ <*x*>)) by FINSEQ_1:def 13;
A72: (Seg (len p)) \ (p " A) c= Seg (len p) by XBOOLE_1:36;
then A73: rng (Sgm ((Seg (len p)) \ (p " A))) c= Seg (len p) by FINSEQ_1:def 13;
assume k in dom (p - A) ; :: thesis: ((p ^ <*x*>) - A) . k = (p - A) . k
then A74: k in dom (Sgm ((Seg (len p)) \ (p " A))) by A57, FUNCT_1:11;
then (Sgm ((Seg (len p)) \ (p " A))) . k in rng (Sgm ((Seg (len p)) \ (p " A))) by FUNCT_1:def 3;
then (Sgm ((Seg (len p)) \ (p " A))) . k in Seg (len p) by A73;
then A75: (Sgm ((Seg (len p)) \ (p " A))) . k in dom p by FINSEQ_1:def 3;
len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = card ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)) by Th37, XBOOLE_1:36
.= (card (Seg (len (p ^ <*x*>)))) - (card ((p ^ <*x*>) " A)) by A48, CARD_2:44 ;
then A76: len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = (len (p ^ <*x*>)) - (card ((p ^ <*x*>) " A)) by FINSEQ_1:57;
A77: dom (Sgm ((Seg (len p)) \ (p " A))) c= dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
proof
<*x*> " A c= dom <*x*> by RELAT_1:132;
then <*x*> " A c= {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then A78: ( <*x*> " A = {} or <*x*> " A = {1} ) by ZFMISC_1:33;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (Sgm ((Seg (len p)) \ (p " A))) or y in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) )
A79: card (p " A) <= (card (p " A)) + 1 by NAT_1:12;
assume A80: y in dom (Sgm ((Seg (len p)) \ (p " A))) ; :: thesis: y in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
then reconsider l = y as Element of NAT ;
A81: y in Seg (len (Sgm ((Seg (len p)) \ (p " A)))) by A80, FINSEQ_1:def 3;
then l <= (len p) - (card (p " A)) by A70, FINSEQ_1:1;
then l + (card (p " A)) <= len p by XREAL_1:19;
then A82: (l + (card (p " A))) + 1 <= len (p ^ <*x*>) by A1, XREAL_1:7;
card ((p ^ <*x*>) " A) = (card (p " A)) + (card (<*x*> " A)) by Th55;
then l + (card ((p ^ <*x*>) " A)) <= l + ((card (p " A)) + 1) by A78, A79, CARD_1:30, XREAL_1:7;
then l + (card ((p ^ <*x*>) " A)) <= len (p ^ <*x*>) by A82, XXREAL_0:2;
then A83: l <= len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by A76, XREAL_1:19;
1 <= l by A81, FINSEQ_1:1;
then l in Seg (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))) by A83, FINSEQ_1:1;
hence y in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by FINSEQ_1:def 3; :: thesis: verum
end;
then (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k in rng (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by A74, FUNCT_1:def 3;
then (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k in Seg (len (p ^ <*x*>)) by A71;
then reconsider l = (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k as Element of NAT ;
dom (p ^ <*x*>) = Seg (len (p ^ <*x*>)) by FINSEQ_1:def 3;
then A84: ((p ^ <*x*>) - A) . k = (p ^ <*x*>) . l by A74, A77, FUNCT_1:13;
(len p) + 1 in Seg ((len p) + 1) by FINSEQ_1:4;
then A85: {((len p) + 1)} c= Seg ((len p) + 1) by ZFMISC_1:31;
A86: now :: thesis: (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k = (Sgm ((Seg (len p)) \ (p " A))) . k
per cases ( (Seg (len p)) \ (p " A) = (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) or (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) = ((Seg (len p)) \ (p " A)) \/ {((len p) + 1)} ) by A37, A49, A58, A68;
suppose (Seg (len p)) \ (p " A) = (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) ; :: thesis: (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k = (Sgm ((Seg (len p)) \ (p " A))) . k
hence (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k = (Sgm ((Seg (len p)) \ (p " A))) . k ; :: thesis: verum
end;
suppose A87: (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) = ((Seg (len p)) \ (p " A)) \/ {((len p) + 1)} ; :: thesis: (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k = (Sgm ((Seg (len p)) \ (p " A))) . k
now :: thesis: for m, n being Nat st m in (Seg (len p)) \ (p " A) & n in {((len p) + 1)} holds
m < n
let m, n be Nat; :: thesis: ( m in (Seg (len p)) \ (p " A) & n in {((len p) + 1)} implies m < n )
assume that
A88: m in (Seg (len p)) \ (p " A) and
A89: n in {((len p) + 1)} ; :: thesis: m < n
m in Seg (len p) by A88, XBOOLE_0:def 5;
then A90: m <= len p by FINSEQ_1:1;
A91: len p < (len p) + 1 by XREAL_1:29;
n = (len p) + 1 by A89, TARSKI:def 1;
hence m < n by A90, A91, XXREAL_0:2; :: thesis: verum
end;
then Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)) = (Sgm ((Seg (len p)) \ (p " A))) ^ (Sgm {((len p) + 1)}) by A72, A85, A87, Th40;
hence (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k = (Sgm ((Seg (len p)) \ (p " A))) . k by A74, FINSEQ_1:def 7; :: thesis: verum
end;
end;
end;
(p - A) . k = p . ((Sgm ((Seg (len p)) \ (p " A))) . k) by A57, A74, FUNCT_1:13;
hence ((p ^ <*x*>) - A) . k = (p - A) . k by A75, A86, A84, FINSEQ_1:def 7; :: thesis: verum
end;
len ((p ^ <*x*>) - A) = (len (p ^ <*x*>)) - (card ((p ^ <*x*>) " A)) by Th57
.= ((len p) + (len <*x*>)) - (card ((p ^ <*x*>) " A)) by FINSEQ_1:22
.= ((len p) + (len <*x*>)) - ((card (p " A)) + (card (<*x*> " A))) by Th55
.= (((len p) - (card (p " A))) + (len <*x*>)) + (- (card (<*x*> " A)))
.= ((len (p - A)) + (len <*x*>)) + (- (card (<*x*> " A))) by Th57
.= (len (p - A)) + ((len <*x*>) - (card (<*x*> " A)))
.= (len (p - A)) + (len (<*x*> - A)) by Th57 ;
hence (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A) by A36, A2, Th36; :: thesis: verum