let f, g be FinSequence; :: thesis: ( dom f = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
f . k = p . k ) & ( for k being Nat st k in dom q holds
f . ((len p) + k) = q . k ) & dom g = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
g . k = p . k ) & ( for k being Nat st k in dom q holds
g . ((len p) + k) = q . k ) implies f = g )
assume that
A18: dom f = Seg ((len p) + (len q)) and
A19: for k being Nat st k in dom p holds
f . k = p . k and
A20: for k being Nat st k in dom q holds
f . ((len p) + k) = q . k and
A21: dom g = Seg ((len p) + (len q)) and
A22: for k being Nat st k in dom p holds
g . k = p . k and
A23: for k being Nat st k in dom q holds
g . ((len p) + k) = q . k ; :: thesis: f = g
for x being object st x in Seg ((len p) + (len q)) holds
f . x = g . x

proof

let x be object ; :: thesis: ( x in Seg ((len p) + (len q)) implies f . x = g . x )
assume A24: x in Seg ((len p) + (len q)) ; :: thesis: f . x = g . x
then reconsider k = x as Element of NAT ;
A25: 1 <= k by A24, Th1;

A26: now :: thesis: ( (len p) + 1 <= k implies f . x = g . x )

assume (len p) + 1 <= k ; :: thesis: f . x = g . x
then consider m being Nat such that
A27: ((len p) + 1) + m = k by NAT_1:10;
(len p) + (1 + m) <= (len p) + (len q) by A24, A27, Th1;
then ( 1 + 0 <= 1 + m & 1 + m <= len q ) by XREAL_1:6;
then 1 + m in Seg (len q) ;
then A28: 1 + m in dom q by Def3;
then g . ((len p) + (1 + m)) = q . (1 + m) by A23;
hence f . x = g . x by A20, A27, A28; :: thesis: verum

end;

now :: thesis: ( not (len p) + 1 <= k implies f . x = g . x )

assume not (len p) + 1 <= k ; :: thesis: f . x = g . x
then k <= len p by NAT_1:8;
then k in Seg (len p) by A25;
then A29: k in dom p by Def3;
then f . k = p . k by A19;
hence f . x = g . x by A22, A29; :: thesis: verum

end;

hence f . x = g . x by A26; :: thesis: verum

end;

hence f = g by A18, A21; :: thesis: verum