let p1, p2 be FinSequence; :: thesis: p1 ^ p2 = p1 \/ ((len p1) Shift p2)
A1: dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2)) by Th62;
dom p1 misses dom ((len p1) Shift p2) by Th63;
then reconsider p = p1 \/ ((len p1) Shift p2) as FinSequence by A1, FINSEQ_1:def 2, GRFUNC_1:31;
A2: dom p = Seg ((len p1) + (len p2)) by Th62;
A3: for k being Nat st k in dom p1 holds
p . k = p1 . k

proof

let k be Nat; :: thesis: ( k in dom p1 implies p . k = p1 . k )
assume k in dom p1 ; :: thesis: p . k = p1 . k
then [k,(p1 . k)] in p1 by FUNCT_1:def 4;
then [k,(p1 . k)] in p by XBOOLE_0:def 3;
hence p . k = p1 . k by FUNCT_1:8; :: thesis: verum

end;

for k being Nat st k in dom p2 holds
p . ((len p1) + k) = p2 . k

proof

let k be Nat; :: thesis: ( k in dom p2 implies p . ((len p1) + k) = p2 . k )
assume A4: k in dom p2 ; :: thesis: p . ((len p1) + k) = p2 . k
dom ((len p1) Shift p2) = { ((len p1) + j) where j is Element of NAT : j in dom p2 } by Def15;
then (len p1) + k in dom ((len p1) Shift p2) by A4;
then [((len p1) + k),(((len p1) Shift p2) . ((len p1) + k))] in (len p1) Shift p2 by FUNCT_1:def 4;
then [((len p1) + k),(((len p1) Shift p2) . ((len p1) + k))] in p by XBOOLE_0:def 3;
then p . ((len p1) + k) = ((len p1) Shift p2) . ((len p1) + k) by FUNCT_1:8;
hence p . ((len p1) + k) = p2 . k by A4, Def15; :: thesis: verum

end;

hence p1 ^ p2 = p1 \/ ((len p1) Shift p2) by A2, A3, FINSEQ_1:def 7; :: thesis: verum