let p1, p2 be FinSequence; :: thesis: dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2))
A6: Seg ((len p1) + (len p2)) = { j where j is Element of NAT : ( 1 <= j & j <= (len p1) + (len p2) ) } by FINSEQ_1:def 1;
A7: dom (p1 \/ ((len p1) Shift p2)) = (dom p1) \/ (dom ((len p1) Shift p2)) by RELAT_1:13;
A8: dom p1 = Seg (len p1) by FINSEQ_1:def 3
.= { k where k is Element of NAT : ( 1 <= k & k <= len p1 ) } by FINSEQ_1:def 1 ;
A9: dom ((len p1) Shift p2) = { k1 where k1 is Element of NAT : ( (len p1) + 1 <= k1 & k1 <= (len p1) + (len p2) ) } by Th54;
thus dom (p1 \/ ((len p1) Shift p2)) c= Seg ((len p1) + (len p2)) :: according to XBOOLE_0:def 10 :: thesis: Seg ((len p1) + (len p2)) c= dom (p1 \/ ((len p1) Shift p2))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (p1 \/ ((len p1) Shift p2)) or x in Seg ((len p1) + (len p2)) )
assume x in dom (p1 \/ ((len p1) Shift p2)) ; :: thesis: x in Seg ((len p1) + (len p2))
then ( x in dom p1 or x in dom ((len p1) Shift p2) ) by A7, XBOOLE_0:def 3;
then A10: ex k3 being Element of NAT st
( ( x = k3 & 1 <= k3 & k3 <= len p1 ) or ( x = k3 & (len p1) + 1 <= k3 & k3 <= (len p1) + (len p2) ) ) by A8, A9;
then reconsider x = x as Element of NAT ;
A11: 1 <= x by A10, Lm2;
x <= (len p1) + (len p2) by A10, Lm2;
hence x in Seg ((len p1) + (len p2)) by A6, A11; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg ((len p1) + (len p2)) or x in dom (p1 \/ ((len p1) Shift p2)) )
assume x in Seg ((len p1) + (len p2)) ; :: thesis: x in dom (p1 \/ ((len p1) Shift p2))
then consider j being Element of NAT such that
A12: x = j and
A13: 1 <= j and
A14: j <= (len p1) + (len p2) by A6;
reconsider i0 = len p1 as Integer ;
( ( 1 <= j & j <= i0 ) or ( i0 + 1 <= j & j <= i0 + (len p2) ) ) by A13, A14, INT_1:20;
then ( x in dom p1 or x in dom ((len p1) Shift p2) ) by A8, A9, A12;
hence x in dom (p1 \/ ((len p1) Shift p2)) by A7, XBOOLE_0:def 3; :: thesis: verum