let p1, p2 be FinSequence; 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))
XBOOLE_0:def 10 Seg ((len p1) + (len p2)) c= dom (p1 \/ (Shift (p2,(len p1))))
let x be object ; TARSKI:def 3 ( 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))
; 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; verum