let G, H be XFinSequence; :: thesis: ( dom G = (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 = (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 = (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 = (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 = (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
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 not i in Segm (len f) ;
then i + (1 - (len f)) >= (len f) + (1 - (len f)) by NAT_1:44, XREAL_1:6;
then reconsider j = (i + 1) - (len f) as non zero Nat ;
i in Segm ((len f) + (len g)) by B1, A1;
then i + (1 - (len f)) < ((len f) + (len g)) + (1 - (len f)) by NAT_1:44, XREAL_1:6;
then j < (len g) + 1 ;
then S1: ( 1 <= j & j <= len g ) by NAT_1:13, NAT_1:14;
then H . (((len f) + j) - 1) = g . j by A2, FINSEQ_3:25
.= G . (((len f) + j) - 1) by A1, S1, FINSEQ_3:25 ;
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