let x, y be set ; :: thesis: for p, q being FinSequence holds ((p ^ <*x*>) ^ q) +* (((len p) + 1),y) = (p ^ <*y*>) ^ q
let p, q be FinSequence; :: thesis: ((p ^ <*x*>) ^ q) +* (((len p) + 1),y) = (p ^ <*y*>) ^ q
A1: dom ((p ^ <*x*>) ^ q) = Seg (len ((p ^ <*x*>) ^ q)) by FINSEQ_1:def 3
.= Seg ((len (p ^ <*x*>)) + (len q)) by FINSEQ_1:22
.= Seg (((len p) + (len <*x*>)) + (len q)) by FINSEQ_1:22
.= Seg (((len p) + 1) + (len q)) by FINSEQ_1:40 ;
A2: dom ((p ^ <*y*>) ^ q) = Seg (len ((p ^ <*y*>) ^ q)) by FINSEQ_1:def 3
.= Seg ((len (p ^ <*y*>)) + (len q)) by FINSEQ_1:22
.= Seg (((len p) + (len <*y*>)) + (len q)) by FINSEQ_1:22
.= Seg (((len p) + 1) + (len q)) by FINSEQ_1:40 ;
A3: dom (((p ^ <*x*>) ^ q) +* (((len p) + 1),y)) = dom ((p ^ <*x*>) ^ q) by FUNCT_7:30;

now :: thesis: for a being object st a in dom ((p ^ <*x*>) ^ q) holds
(((p ^ <*x*>) ^ q) +* (((len p) + 1),y)) . a = ((p ^ <*y*>) ^ q) . a

let a be object ; :: thesis: ( a in dom ((p ^ <*x*>) ^ q) implies (((p ^ <*x*>) ^ q) +* (((len p) + 1),y)) . b₁ = ((p ^ <*y*>) ^ q) . b₁ )
assume A4: a in dom ((p ^ <*x*>) ^ q) ; :: thesis: (((p ^ <*x*>) ^ q) +* (((len p) + 1),y)) . b₁ = ((p ^ <*y*>) ^ q) . b₁
then reconsider i = a as Nat ;
A5: ( i >= 1 & i <= len ((p ^ <*x*>) ^ q) ) by A4, FINSEQ_3:25;

per cases ( i < (len p) + 1 or i = (len p) + 1 or i > (len p) + 1 ) by XXREAL_0:1;

suppose A6: i < (len p) + 1 ; :: thesis: (((p ^ <*x*>) ^ q) +* (((len p) + 1),y)) . b₁ = ((p ^ <*y*>) ^ q) . b₁

then i <= len p by NAT_1:13;
then ( i in dom p & dom p c= dom (p ^ <*x*>) & dom p c= dom (p ^ <*y*>) ) by A5, FINSEQ_1:26, FINSEQ_3:25;
then ( (p ^ <*x*>) . i = p . i & ((p ^ <*x*>) ^ q) . i = (p ^ <*x*>) . i & (len p) + 1 <> i & (p ^ <*y*>) . i = p . i & ((p ^ <*y*>) ^ q) . i = (p ^ <*y*>) . i ) by A6, FINSEQ_1:def 7;
hence (((p ^ <*x*>) ^ q) +* (((len p) + 1),y)) . a = ((p ^ <*y*>) ^ q) . a by FUNCT_7:32; :: thesis: verum

end;

suppose A7: i = (len p) + 1 ; :: thesis: (((p ^ <*x*>) ^ q) +* (((len p) + 1),y)) . b₁ = ((p ^ <*y*>) ^ q) . b₁

( len <*x*> = 1 & len <*y*> = 1 ) by FINSEQ_1:40;
then ( i >= 1 & len (p ^ <*x*>) = (len p) + 1 & len (p ^ <*y*>) = (len p) + 1 ) by A7, FINSEQ_1:22, NAT_1:11;
then ( i in dom (p ^ <*x*>) & i in dom (p ^ <*y*>) ) by A7, FINSEQ_3:25;
then ( ((p ^ <*x*>) ^ q) . i = (p ^ <*x*>) . i & (p ^ <*x*>) . i = x & ((p ^ <*y*>) ^ q) . i = (p ^ <*y*>) . i & (p ^ <*y*>) . i = y ) by A7, FINSEQ_1:def 7, FINSEQ_1:42;
hence (((p ^ <*x*>) ^ q) +* (((len p) + 1),y)) . a = ((p ^ <*y*>) ^ q) . a by A4, A7, FUNCT_7:31; :: thesis: verum

end;

suppose A8: i > (len p) + 1 ; :: thesis: (((p ^ <*x*>) ^ q) +* (((len p) + 1),y)) . b₁ = ((p ^ <*y*>) ^ q) . b₁

then i >= ((len p) + 1) + 1 by NAT_1:13;
then consider j being Nat such that
A9: i = (((len p) + 1) + 1) + j by NAT_1:10;
A10: i = ((len p) + 1) + (1 + j) by A9;
( len <*x*> = 1 & len <*y*> = 1 ) by FINSEQ_1:40;
then A11: ( len (p ^ <*x*>) = (len p) + 1 & len (p ^ <*y*>) = (len p) + 1 ) by FINSEQ_1:22;
then len ((p ^ <*x*>) ^ q) = ((len p) + 1) + (len q) by FINSEQ_1:22;
then ( 1 <= 1 + j & 1 + j <= len q ) by A10, A4, FINSEQ_3:25, XREAL_1:6, NAT_1:11;
then 1 + j in dom q by FINSEQ_3:25;
then ( ((p ^ <*x*>) ^ q) . i = q . (1 + j) & ((p ^ <*y*>) ^ q) . i = q . (1 + j) ) by A10, A11, FINSEQ_1:def 7;
hence (((p ^ <*x*>) ^ q) +* (((len p) + 1),y)) . a = ((p ^ <*y*>) ^ q) . a by A8, FUNCT_7:32; :: thesis: verum

end;

end;

end;

hence ((p ^ <*x*>) ^ q) +* (((len p) + 1),y) = (p ^ <*y*>) ^ q by A1, A2, A3; :: thesis: verum