let p1, p2 be FinSequence; :: thesis: dom (p1 \/ (Shift (p2,(len p1)))) = Seg ((len p1) + (len p2))
A1: dom (p1 \/ (Shift (p2,(len p1)))) = (dom p1) \/ (dom (Shift (p2,(len p1)))) by XTUPLE_0:23;
A2: dom p1 = Seg (len p1) by FINSEQ_1:def 3
.= { k where k is Nat : ( 1 <= k & k <= len p1 ) } ;
A3: dom (Shift (p2,(len p1))) = { k1 where k1 is Nat : ( (len p1) + 1 <= k1 & k1 <= (len p1) + (len p2) ) } by Th39;
thus dom (p1 \/ (Shift (p2,(len p1)))) c= Seg ((len p1) + (len p2)) :: according to XBOOLE_0:def 10 :: thesis: Seg ((len p1) + (len p2)) c= dom (p1 \/ (Shift (p2,(len p1))))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (p1 \/ (Shift (p2,(len p1)))) or x in Seg ((len p1) + (len p2)) )
assume x in dom (p1 \/ (Shift (p2,(len p1)))) ; :: thesis: x in Seg ((len p1) + (len p2))
then A4: ( x in dom p1 or x in dom (Shift (p2,(len p1))) ) by A1, XBOOLE_0:def 3;
then A5: ex k3 being Nat st
( ( x = k3 & 1 <= k3 & k3 <= len p1 ) or ( x = k3 & (len p1) + 1 <= k3 & k3 <= (len p1) + (len p2) ) ) by A2, A3;
reconsider x = x as Nat by A4;
A6: 1 <= x by A5, Lm6;
x <= (len p1) + (len p2) by A5, Lm6;
hence x in Seg ((len p1) + (len p2)) by A6; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg ((len p1) + (len p2)) or x in dom (p1 \/ (Shift (p2,(len p1)))) )
assume x in Seg ((len p1) + (len p2)) ; :: thesis: x in dom (p1 \/ (Shift (p2,(len p1))))
then consider j being Nat such that
A7: x = j and
A8: 1 <= j and
A9: j <= (len p1) + (len p2) ;
reconsider i0 = len p1 as Integer ;
( ( 1 <= j & j <= i0 ) or ( i0 + 1 <= j & j <= i0 + (len p2) ) ) by A8, A9, INT_1:7;
then ( x in dom p1 or x in dom (Shift (p2,(len p1))) ) by A2, A3, A7;
hence x in dom (p1 \/ (Shift (p2,(len p1)))) by A1, XBOOLE_0:def 3; :: thesis: verum