let G, H be FinSequence; :: thesis: ( dom G = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
G . k = f . k ) & ( for k being Nat st k in dom g holds
G . (((len f) + k) + 1) = g . k ) & dom H = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
H . k = f . k ) & ( for k being Nat st k in dom g holds
H . (((len f) + k) + 1) = g . k ) implies G = H )
assume A1: ( dom G = Seg ((len f) + (len g)) & ( for i being Nat st i in dom f holds
G . i = f . i ) & ( for i being Nat st i in dom g holds
G . (((len f) + i) + 1) = g . i ) ) ; :: thesis: ( not dom H = Seg ((len f) + (len g)) or ex k being Nat st
( k in dom f & not H . k = f . k ) or ex k being Nat st
( k in dom g & not H . (((len f) + k) + 1) = g . k ) or G = H )
assume A2: ( dom H = Seg ((len f) + (len g)) & ( for i being Nat st i in dom f holds
H . i = f . i ) & ( for i being Nat st i in dom g holds
H . (((len f) + i) + 1) = g . i ) ) ; :: thesis: G = H
for i being object st i in dom G holds
G . i = H . i

proof

let i be object ; :: thesis: ( i in dom G implies G . i = H . i )
assume B1: i in dom G ; :: thesis: G . i = H . i
B2: len G = (len f) + (len g) by A1, FINSEQ_1:def 3;
reconsider i = i as Nat by B1;
H . i = G . i

proof

per cases ( i in dom f or not i in dom f ) ;

suppose C1: i in dom f ; :: thesis: H . i = G . i

then H . i = f . i by A2
.= G . i by A1, C1 ;
hence H . i = G . i ; :: thesis: verum

end;

suppose not i in dom f ; :: thesis: H . i = G . i

then C0: ( ( i < 1 or len f < i ) & 1 <= i & i <= len G ) by B1, FINSEQ_3:25;
then (len f) + 1 <= i by NAT_1:13;
then ((len f) + 1) - ((len f) + 1) <= i - ((len f) + 1) by XREAL_1:9;
then reconsider j = i - ((len f) + 1) as Nat by INT_1:3;
i - ((len f) + 1) <= ((len f) + (len g)) - ((len f) + 1) by B2, C0, XREAL_1:9;
then j < ((len g) - 1) + 1 by NAT_1:13;
then C1: j in Segm (len g) by NAT_1:44;
then H . (((len f) + j) + 1) = g . j by A2
.= G . (((len f) + j) + 1) by A1, C1 ;
hence H . i = G . i ; :: thesis: verum

end;

end;

end;

hence G . i = H . i ; :: thesis: verum

end;

hence G = H by A1, A2; :: thesis: verum