let p be FinSequence; :: thesis: for x, A being set holds (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)
let x, 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:35
.= (len p) + 1 by FINSEQ_1:57 ;
A2: len ((p ^ <*x*>) - A) = (len (p ^ <*x*>)) - (card ((p ^ <*x*>) " A)) by Th66
.= ((len p) + (len <*x*>)) - (card ((p ^ <*x*>) " A)) by FINSEQ_1:35
.= ((len p) + (len <*x*>)) - ((card (p " A)) + (card (<*x*> " A))) by Th63
.= (((len p) - (card (p " A))) + (len <*x*>)) + (- (card (<*x*> " A)))
.= ((len (p - A)) + (len <*x*>)) + (- (card (<*x*> " A))) by Th66
.= (len (p - A)) + ((len <*x*>) - (card (<*x*> " A)))
.= (len (p - A)) + (len (<*x*> - A)) by Th66 ;

A3: now

let k be Element of NAT ; :: thesis: ( k in dom (p - A) implies ((p ^ <*x*>) - A) . k = (p - A) . k )
assume A4: k in dom (p - A) ; :: thesis: ((p ^ <*x*>) - A) . k = (p - A) . k
set s1 = Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A));
set s2 = Sgm ((Seg (len p)) \ (p " A));
A5: dom (p ^ <*x*>) = Seg (len (p ^ <*x*>)) by FINSEQ_1:def 3;
A6: dom p = Seg (len p) by FINSEQ_1:def 3;
then A7: k in dom (Sgm ((Seg (len p)) \ (p " A))) by A4, FUNCT_1:21;
(p ^ <*x*>) " A c= dom (p ^ <*x*>) by RELAT_1:167;
then A8: (p ^ <*x*>) " A c= Seg (len (p ^ <*x*>)) by FINSEQ_1:def 3;
len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = card ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)) by Th44, XBOOLE_1:36
.= (card (Seg (len (p ^ <*x*>)))) - (card ((p ^ <*x*>) " A)) by A8, CARD_2:63 ;
then A9: len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = (len (p ^ <*x*>)) - (card ((p ^ <*x*>) " A)) by FINSEQ_1:78;
p " A c= dom p by RELAT_1:167;
then A10: 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 Th44, XBOOLE_1:36
.= (card (Seg (len p))) - (card (p " A)) by A10, CARD_2:63 ;
then A11: len (Sgm ((Seg (len p)) \ (p " A))) = (len p) - (card (p " A)) by FINSEQ_1:78;
A12: dom (Sgm ((Seg (len p)) \ (p " A))) c= dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))

proof

let y be set ; :: 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))) )
assume A13: 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 ;
A14: y in Seg (len (Sgm ((Seg (len p)) \ (p " A)))) by A13, FINSEQ_1:def 3;
then A15: ( 1 <= l & l <= len (Sgm ((Seg (len p)) \ (p " A))) ) by FINSEQ_1:3;
l <= (len p) - (card (p " A)) by A11, A14, FINSEQ_1:3;
then l + (card (p " A)) <= len p by XREAL_1:21;
then A16: (l + (card (p " A))) + 1 <= len (p ^ <*x*>) by A1, XREAL_1:9;
A17: card ((p ^ <*x*>) " A) = (card (p " A)) + (card (<*x*> " A)) by Th63;
<*x*> " A c= dom <*x*> by RELAT_1:167;
then <*x*> " A c= {1} by FINSEQ_1:4, FINSEQ_1:def 8;
then ( <*x*> " A = {} or <*x*> " A = {1} ) by ZFMISC_1:39;
then ( ( card ((p ^ <*x*>) " A) = card (p " A) or card ((p ^ <*x*>) " A) = (card (p " A)) + 1 ) & card ((p ^ <*x*>) " A) <= card ((p ^ <*x*>) " A) & card (p " A) <= (card (p " A)) + 1 ) by A17, CARD_1:47, CARD_1:50, NAT_1:12;
then l + (card ((p ^ <*x*>) " A)) <= l + ((card (p " A)) + 1) by XREAL_1:9;
then l + (card ((p ^ <*x*>) " A)) <= len (p ^ <*x*>) by A16, XXREAL_0:2;
then l <= len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by A9, XREAL_1:21;
then l in Seg (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))) by A15, FINSEQ_1:3;
hence y in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by FINSEQ_1:def 3; :: thesis: verum

end;

A18: (Seg (len p)) \ (p " A) c= Seg (len p) by XBOOLE_1:36;
then ( (Sgm ((Seg (len p)) \ (p " A))) . k in rng (Sgm ((Seg (len p)) \ (p " A))) & rng (Sgm ((Seg (len p)) \ (p " A))) c= Seg (len p) ) by A7, FINSEQ_1:def 13, FUNCT_1:def 5;
then (Sgm ((Seg (len p)) \ (p " A))) . k in Seg (len p) ;
then A20: (Sgm ((Seg (len p)) \ (p " A))) . k in dom p by FINSEQ_1:def 3;
(Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) c= Seg (len (p ^ <*x*>)) by XBOOLE_1:36;
then ( (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k in rng (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) & rng (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) c= Seg (len (p ^ <*x*>)) ) by A7, A12, FINSEQ_1:def 13, FUNCT_1:def 5;
then (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k in Seg (len (p ^ <*x*>)) ;
then reconsider l = (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k as Element of NAT ;
A21: ( x in A implies (p ^ <*x*>) " A = (p " A) \/ {((len p) + 1)} )

proof

assume A22: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in (p ^ <*x*>) " A or y in (p " A) \/ {((len p) + 1)} )
assume A23: y in (p ^ <*x*>) " A ; :: thesis: y in (p " A) \/ {((len p) + 1)}
then y in dom (p ^ <*x*>) by FUNCT_1:def 13;
then y in Seg ((len p) + 1) by A1, FINSEQ_1:def 3;
then A24: y in (Seg (len p)) \/ {((len p) + 1)} by FINSEQ_1:11;

now

per cases ( y in Seg (len p) or y in {((len p) + 1)} ) by A24, XBOOLE_0:def 3;

suppose A25: y in Seg (len p) ; :: thesis: y in (p " A) \/ {((len p) + 1)}

then A26: y in dom p by FINSEQ_1:def 3;
reconsider j = y as Element of NAT by A25;
( p . j = (p ^ <*x*>) . j & (p ^ <*x*>) . y in A ) by A23, A26, FINSEQ_1:def 7, FUNCT_1:def 13;
then y in p " A by A26, FUNCT_1:def 13;
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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in (p " A) \/ {((len p) + 1)} or y in (p ^ <*x*>) " A )
assume A27: y in (p " A) \/ {((len p) + 1)} ; :: thesis: y in (p ^ <*x*>) " A

now

per cases ( y in p " A or y in {((len p) + 1)} ) by A27, XBOOLE_0:def 3;

suppose A28: y in p " A ; :: thesis: y in (p ^ <*x*>) " A

p " A c= (p ^ <*x*>) " A by Th64;
hence y in (p ^ <*x*>) " A by A28; :: thesis: verum

end;

suppose y in {((len p) + 1)} ; :: thesis: y in (p ^ <*x*>) " A

then y = (len p) + 1 by TARSKI:def 1;
then ( y in Seg (len (p ^ <*x*>)) & (p ^ <*x*>) . y in A ) by A1, A22, FINSEQ_1:6, FINSEQ_1:59;
then ( y in dom (p ^ <*x*>) & (p ^ <*x*>) . y in A ) by FINSEQ_1:def 3;
hence y in (p ^ <*x*>) " A by FUNCT_1:def 13; :: thesis: verum

end;

end;

end;

hence y in (p ^ <*x*>) " A ; :: thesis: verum

end;

A29: ( not x in A implies (p ^ <*x*>) " A = p " A )

proof

assume A30: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in (p ^ <*x*>) " A or y in p " A )
assume A31: y in (p ^ <*x*>) " A ; :: thesis: y in p " A
then A32: y in dom (p ^ <*x*>) by FUNCT_1:def 13;
then reconsider l = y as Element of NAT ;
y in Seg (len (p ^ <*x*>)) by A32, FINSEQ_1:def 3;
then A33: ( 1 <= l & l <= (len p) + 1 ) by A1, FINSEQ_1:3;

now

assume l = (len p) + 1 ; :: thesis: contradiction
then ( (p ^ <*x*>) . l = x & l in (p ^ <*x*>) " A ) by A31, FINSEQ_1:59;
hence contradiction by A30, FUNCT_1:def 13; :: thesis: verum

end;

then l < (len p) + 1 by A33, XXREAL_0:1;
then l <= len p by NAT_1:13;
then l in Seg (len p) by A33, FINSEQ_1:3;
then ( y in dom p & (p ^ <*x*>) . l in A ) by A31, FINSEQ_1:def 3, FUNCT_1:def 13;
then ( y in dom p & p . l in A ) by FINSEQ_1:def 7;
hence y in p " A by FUNCT_1:def 13; :: thesis: verum

end;

thus p " A c= (p ^ <*x*>) " A by Th64; :: thesis: verum

end;

A34: now

assume A35: (p ^ <*x*>) " A = p " A ; :: thesis: (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) = ((Seg (len p)) \ (p " A)) \/ {((len p) + 1)}
{((len p) + 1)} /\ (p " A) = {}

proof

assume A36: not {((len p) + 1)} /\ (p " A) = {} ; :: thesis: contradiction
consider z being Element of {((len p) + 1)} /\ (p " A);
z in {((len p) + 1)} by A36, XBOOLE_0:def 4;
then A37: z = (len p) + 1 by TARSKI:def 1;
( p " A c= dom p & dom p = Seg (len p) & z in p " A ) by A36, FINSEQ_1:def 3, RELAT_1:167, XBOOLE_0:def 4;
then ( (len p) + 1 <= len p & len p < (len p) + 1 ) by A37, FINSEQ_1:3, XREAL_1:31;
hence contradiction ; :: thesis: verum

end;

then A38: {((len p) + 1)} misses p " A by XBOOLE_0:def 7;
thus (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) = ((Seg (len p)) \/ {((len p) + 1)}) \ (p " A) by A1, A35, FINSEQ_1:11
.= ((Seg (len p)) \ (p " A)) \/ ({((len p) + 1)} \ (p " A)) by XBOOLE_1:42
.= ((Seg (len p)) \ (p " A)) \/ {((len p) + 1)} by A38, XBOOLE_1:83 ; :: thesis: verum

end;

(Seg (len p)) /\ {((len p) + 1)} = {}

proof

assume A39: not (Seg (len p)) /\ {((len p) + 1)} = {} ; :: thesis: contradiction
consider z being Element of (Seg (len p)) /\ {((len p) + 1)};
A40: z in Seg (len p) by A39, XBOOLE_0:def 4;
then reconsider f = z as Element of NAT ;
f in {((len p) + 1)} by A39, XBOOLE_0:def 4;
then ( f = (len p) + 1 & f <= len p ) by A40, FINSEQ_1:3, TARSKI:def 1;
hence contradiction by XREAL_1:31; :: thesis: verum

end;

then A41: Seg (len p) misses {((len p) + 1)} by XBOOLE_0:def 7;

A42: now

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:11
.= ((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 A41, XBOOLE_1:83
.= (Seg (len p)) \ (p " A) by XBOOLE_1:28, XBOOLE_1:36 ;
:: thesis: verum

end;

(len p) + 1 in Seg ((len p) + 1) by FINSEQ_1:6;
then A43: {((len p) + 1)} c= Seg ((len p) + 1) by ZFMISC_1:37;

A44: now

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 A21, A29, A34, A42;

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 A45: (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

let m, n be Element of NAT ; :: thesis: ( m in (Seg (len p)) \ (p " A) & n in {((len p) + 1)} implies m < n )
assume that
A46: m in (Seg (len p)) \ (p " A) and
A47: n in {((len p) + 1)} ; :: thesis: m < n
m in Seg (len p) by A46, XBOOLE_0:def 5;
then ( m <= len p & n = (len p) + 1 & len p < (len p) + 1 ) by A47, FINSEQ_1:3, TARSKI:def 1, XREAL_1:31;
hence m < n by 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 A18, A43, A45, Th48;
hence (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k = (Sgm ((Seg (len p)) \ (p " A))) . k by A7, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

A48: ((p ^ <*x*>) - A) . k = (p ^ <*x*>) . l by A5, A7, A12, FUNCT_1:23;
(p - A) . k = p . ((Sgm ((Seg (len p)) \ (p " A))) . k) by A6, A7, FUNCT_1:23;
hence ((p ^ <*x*>) - A) . k = (p - A) . k by A20, A44, A48, FINSEQ_1:def 7; :: thesis: verum

end;

now

let k be Element of NAT ; :: thesis: ( k in dom (<*x*> - A) implies ((p ^ <*x*>) - A) . ((len (p - A)) + k) = (<*x*> - A) . k )
assume A49: k in dom (<*x*> - A) ; :: thesis: ((p ^ <*x*>) - A) . ((len (p - A)) + k) = (<*x*> - A) . k
A50: not x in A by Lm7, A49, RELAT_1:60;
then A51: <*x*> - A = <*x*> by Lm6;
then A52: dom (<*x*> - A) = {1} by FINSEQ_1:4, FINSEQ_1:def 8;
then A53: k = 1 by A49, TARSKI:def 1;
A54: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in p " A or y in (p ^ <*x*>) " A )
assume y in p " A ; :: thesis: y in (p ^ <*x*>) " A
then A55: ( y in dom p & p . y in A ) by FUNCT_1:def 13;
then reconsider z = y as Element of NAT ;
( y in dom (p ^ <*x*>) & (p ^ <*x*>) . z in A ) by A55, Th24, FINSEQ_1:def 7;
hence y in (p ^ <*x*>) " A by FUNCT_1:def 13; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (p ^ <*x*>) " A or y in p " A )
assume y in (p ^ <*x*>) " A ; :: thesis: y in p " A
then A56: ( y in dom (p ^ <*x*>) & (p ^ <*x*>) . y in A ) by FUNCT_1:def 13;
then reconsider z = y as Element of NAT ;
A57: ( z in dom p or ex n being Nat st
( n in dom (<*x*> - A) & z = (len p) + n ) ) by A51, A56, FINSEQ_1:38;

A58: now

given n being natural number such that A59: n in dom (<*x*> - A) and
A60: z = (len p) + n ; :: thesis: contradiction
n = 1 by A52, A59, TARSKI:def 1;
hence contradiction by A50, A56, A60, FINSEQ_1:59; :: thesis: verum

end;

then (p ^ <*x*>) . z = p . z by A57, FINSEQ_1:def 7;
hence y in p " A by A56, A57, A58, FUNCT_1:def 13; :: thesis: verum

end;

A61: (len (p - A)) + k = ((len p) - (card (p " A))) + k by Th66
.= ((len p) + 1) - (card ((p ^ <*x*>) " A)) by A53, A54
.= ((len p) + (len <*x*>)) - (card ((p ^ <*x*>) " A)) by FINSEQ_1:56
.= (len (p ^ <*x*>)) - (card ((p ^ <*x*>) " A)) by FINSEQ_1:35
.= len ((p ^ <*x*>) - A) by Th66 ;
set s = Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A));
set S = (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A);
(p ^ <*x*>) " A c= dom (p ^ <*x*>) by RELAT_1:167;
then A62: ( (p ^ <*x*>) " A c= Seg (len (p ^ <*x*>)) & Seg (len (p ^ <*x*>)) is finite ) by FINSEQ_1:def 3;
A63: (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) c= Seg (len (p ^ <*x*>)) by XBOOLE_1:36;
A64: len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = card ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)) by Th44, XBOOLE_1:36
.= (card (Seg (len (p ^ <*x*>)))) - (card ((p ^ <*x*>) " A)) by A62, CARD_2:63
.= (len (p ^ <*x*>)) - (card (p " A)) by A54, FINSEQ_1:78
.= ((len p) - (card (p " A))) + k by A1, A53
.= len ((p ^ <*x*>) - A) by A61, Th66 ;
then A65: ( len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = (len (p - A)) + 1 & dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = Seg (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))) ) by A49, A52, A61, FINSEQ_1:def 3, TARSKI:def 1;
then A66: len ((p ^ <*x*>) - A) in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by A64, FINSEQ_1:6;
A67: dom (p ^ <*x*>) = Seg (len (p ^ <*x*>)) by FINSEQ_1:def 3;
A68: len (p ^ <*x*>) in Seg (len (p ^ <*x*>)) by A1, FINSEQ_1:6;

now

assume A69: len (p ^ <*x*>) in (p ^ <*x*>) " A ; :: thesis: contradiction
(p ^ <*x*>) . (len (p ^ <*x*>)) = x by A1, FINSEQ_1:59;
hence contradiction by A50, A69, FUNCT_1:def 13; :: thesis: verum

end;

then len (p ^ <*x*>) in (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) by A68, XBOOLE_0:def 5;
then len (p ^ <*x*>) in rng (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by A63, FINSEQ_1:def 13;
then consider y being set such that
A70: y in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) and
A71: (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . y = len (p ^ <*x*>) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A70;

now

assume A72: y <> len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) ; :: thesis: contradiction
A73: y in Seg (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))) by A70, FINSEQ_1:def 3;
then y <= len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) by FINSEQ_1:3;
then A74: ( 1 <= y & y < len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) & len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) <= len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) ) by A72, A73, FINSEQ_1:3, XXREAL_0:1;
A75: ( (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))) & rng (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) c= NAT ) by A64, A66, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider w = (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))) as Element of NAT ;
A76: len (p ^ <*x*>) < w by A63, A71, A74, FINSEQ_1:def 13;
w in (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) by A63, A75, FINSEQ_1:def 13;
then w in Seg (len (p ^ <*x*>)) by XBOOLE_0:def 5;
hence contradiction by A76, FINSEQ_1:3; :: thesis: verum

end;

hence ((p ^ <*x*>) - A) . ((len (p - A)) + k) = (p ^ <*x*>) . (len (p ^ <*x*>)) by A61, A64, A65, A67, A71, FINSEQ_1:6, FUNCT_1:23
.= x by A1, FINSEQ_1:59
.= (<*x*> - A) . k by A51, A53, FINSEQ_1:def 8 ;
:: thesis: verum

end;

hence (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A) by A2, A3, Th43; :: thesis: verum