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
A19: ( 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 ) ) and
A20: ( 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 ) ) ; :: thesis: f = g
for x being set st x in Seg ((len p) + (len q)) holds
f . x = g . x

proof

let x be set ; :: thesis: ( x in Seg ((len p) + (len q)) implies f . x = g . x )
assume A21: x in Seg ((len p) + (len q)) ; :: thesis: f . x = g . x
then reconsider k = x as Element of NAT ;
A22: ( 1 <= k & k <= (len p) + (len q) ) by A21, Th3;

A23: now

assume (len p) + 1 <= k ; :: thesis: f . x = g . x
then consider m being Nat such that
A24: ((len p) + 1) + m = k by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A25: 1 + 0 <= 1 + m by XREAL_1:9;
(len p) + (1 + m) <= (len p) + (len q) by A21, A24, Th3;
then 1 + m <= len q by XREAL_1:8;
then 1 + m in Seg (len q) by A25;
then A26: 1 + m in dom q by Def3;
then g . ((len p) + (1 + m)) = q . (1 + m) by A20;
hence f . x = g . x by A19, A24, A26; :: thesis: verum

end;

now

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 A22;
then A27: k in dom p by Def3;
then f . k = p . k by A19;
hence f . x = g . x by A20, A27; :: thesis: verum

end;

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

end;

hence f = g by A19, A20, FUNCT_1:9; :: thesis: verum