let p1, p2 be FinSequence; :: thesis: for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2)
let q1, q2 be FinSubsequence; :: thesis: ( q1 c= p1 & q2 c= p2 implies dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2) )
assume ( q1 c= p1 & q2 c= p2 ) ; :: thesis: dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2)
then A1: ( dom q1 c= dom p1 & dom q2 c= dom p2 ) by GRFUNC_1:8;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (q1 \/ ((len p1) Shift q2)) or x in dom (p1 ^ p2) )
assume x in dom (q1 \/ ((len p1) Shift q2)) ; :: thesis: x in dom (p1 ^ p2)
then A2: x in (dom q1) \/ (dom ((len p1) Shift q2)) by RELAT_1:13;
A3: dom (p1 ^ p2) = Seg ((len p1) + (len p2)) by FINSEQ_1:def 7;

A4: now

assume A5: x in dom q1 ; :: thesis: x in dom (p1 ^ p2)
A6: dom p1 = Seg (len p1) by FINSEQ_1:def 3;
len p1 <= (len p1) + (len p2) by INT_1:19;
then Seg (len p1) c= Seg ((len p1) + (len p2)) by FINSEQ_1:7;
hence x in dom (p1 ^ p2) by A1, A3, A5, A6, TARSKI:def 3; :: thesis: verum

end;

now

assume A7: x in dom ((len p1) Shift q2) ; :: thesis: x in dom (p1 ^ p2)
A8: dom ((len p1) Shift q2) c= dom ((len p1) Shift p2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((len p1) Shift q2) or x in dom ((len p1) Shift p2) )
assume A9: x in dom ((len p1) Shift q2) ; :: thesis: x in dom ((len p1) Shift p2)
A10: dom ((len p1) Shift p2) = { ((len p1) + k) where k is Element of NAT : k in dom p2 } by Def15;
dom ((len p1) Shift q2) = { ((len p1) + k) where k is Element of NAT : k in dom q2 } by Def15;
then consider k being Element of NAT such that
A11: ( x = (len p1) + k & k in dom q2 ) by A9;
thus x in dom ((len p1) Shift p2) by A1, A10, A11; :: thesis: verum

end;

dom (p1 ^ p2) = dom (p1 \/ ((len p1) Shift p2)) by Th64
.= (dom p1) \/ (dom ((len p1) Shift p2)) by RELAT_1:13 ;
then dom ((len p1) Shift p2) c= dom (p1 ^ p2) by XBOOLE_1:7;
then dom ((len p1) Shift q2) c= dom (p1 ^ p2) by A8, XBOOLE_1:1;
hence x in dom (p1 ^ p2) by A7; :: thesis: verum

end;

hence x in dom (p1 ^ p2) by A2, A4, XBOOLE_0:def 3; :: thesis: verum