let p1, p2 be FinSequence; :: thesis: p1 ^ p2 = p1 \/ (Shift (p2,(len p1)))
A1: dom (p1 \/ (Shift (p2,(len p1)))) = Seg ((len p1) + (len p2)) by Th46;
dom p1 misses dom (Shift (p2,(len p1))) by Th47;
then reconsider p = p1 \/ (Shift (p2,(len p1))) as FinSequence by A1, FINSEQ_1:def 2, GRFUNC_1:13;
A2: dom p = Seg ((len p1) + (len p2)) by Th46;
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 2;
then [k,(p1 . k)] in p by XBOOLE_0:def 3;
hence p . k = p1 . k by FUNCT_1:1; :: 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 (Shift (p2,(len p1))) = { (j + (len p1)) where j is Nat : j in dom p2 } by Def12;
then (len p1) + k in dom (Shift (p2,(len p1))) by A4;
then [((len p1) + k),((Shift (p2,(len p1))) . ((len p1) + k))] in Shift (p2,(len p1)) by FUNCT_1:def 2;
then [((len p1) + k),((Shift (p2,(len p1))) . ((len p1) + k))] in p by XBOOLE_0:def 3;
then p . ((len p1) + k) = (Shift (p2,(len p1))) . ((len p1) + k) by FUNCT_1:1;
hence p . ((len p1) + k) = p2 . k by A4, Def12; :: thesis: verum

end;

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