let p1, p2 be FinSequence; :: thesis: dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2))

per cases ( ( p1 = {} & p2 = {} ) or ( p1 <> {} & p2 = {} ) or ( p1 = {} & p2 <> {} ) or ( p1 <> {} & p2 <> {} ) ) ;

suppose A1: ( p1 = {} & p2 = {} ) ; :: thesis: dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2))

then A2: dom (p1 \/ ((len p1) Shift p2)) = dom p1 by Th55;
len p2 = 0 by A1;
hence dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2)) by A2, FINSEQ_1:def 3; :: thesis: verum

end;

suppose A3: ( p1 <> {} & p2 = {} ) ; :: thesis: dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2))

then A4: (len p1) Shift p2 = {} by Th55;
len p2 = 0 by A3;
hence dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2)) by A4, FINSEQ_1:def 3; :: thesis: verum

end;

suppose A5: ( p1 = {} & p2 <> {} ) ; :: thesis: dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2))

then dom (p1 \/ ((len p1) Shift p2)) = dom (0 Shift p2)
.= dom p2 by Th52
.= Seg (0 + (len p2)) by FINSEQ_1:def 3
.= Seg ((len p1) + (len p2)) by A5 ;
hence dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2)) ; :: thesis: verum

end;

suppose A6: ( p1 <> {} & p2 <> {} ) ; :: thesis: dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2))

A7: Seg ((len p1) + (len p2)) = { j where j is Element of NAT : ( 1 <= j & j <= (len p1) + (len p2) ) } by FINSEQ_1:def 1;
A8: dom (p1 \/ ((len p1) Shift p2)) = (dom p1) \/ (dom ((len p1) Shift p2)) by RELAT_1:13;
A9: 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 ;
A10: dom ((len p1) Shift p2) = { k1 where k1 is Element of NAT : ( (len p1) + 1 <= k1 & k1 <= (len p1) + (len p2) ) } by A6, 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 A8, XBOOLE_0:def 3;
then consider k3 being Element of NAT such that
A11: ( ( x = k3 & 1 <= k3 & k3 <= len p1 ) or ( x = k3 & (len p1) + 1 <= k3 & k3 <= (len p1) + (len p2) ) ) by A9, A10;
reconsider x = x as Element of NAT by A11;
( 1 <= x & x <= (len p1) + (len p2) ) by A11, Lm2;
hence x in Seg ((len p1) + (len p2)) by A7; :: 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 & 1 <= j & j <= (len p1) + (len p2) ) by A7;
reconsider i0 = len p1 as Integer ;
( ( 1 <= j & j <= i0 ) or ( i0 + 1 <= j & j <= i0 + (len p2) ) ) by A12, INT_1:20;
then ( x in dom p1 or x in dom ((len p1) Shift p2) ) by A9, A10, A12;
hence x in dom (p1 \/ ((len p1) Shift p2)) by A8, XBOOLE_0:def 3; :: thesis: verum

end;

end;