let i be Element of NAT ; :: thesis: for q, q1, q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds
(i Shift q1) \/ (i Shift q2) = i Shift q
let q, q1, q2 be FinSubsequence; :: thesis: ( q = q1 \/ q2 & q1 misses q2 implies (i Shift q1) \/ (i Shift q2) = i Shift q )
assume that
A1: q = q1 \/ q2 and
A2: q1 misses q2 ; :: thesis: (i Shift q1) \/ (i Shift q2) = i Shift q
A3: dom (i Shift q) = { (i + k) where k is Element of NAT : k in dom q } by Def15;
A4: dom (i Shift q1) = { (i + k) where k is Element of NAT : k in dom q1 } by Def15;
A5: dom (i Shift q2) = { (i + k) where k is Element of NAT : k in dom q2 } by Def15;
A6: ( q1 c= q & q2 c= q ) by A1, XBOOLE_1:7;
A7: ( i Shift q1 c= i Shift q & i Shift q2 c= i Shift q ) by A1, Th70, XBOOLE_1:7;
dom q1 misses dom q2 by A2, A6, Th10;
then dom (i Shift q1) misses dom (i Shift q2) by Th72;
then reconsider q3 = (i Shift q1) \/ (i Shift q2) as Function by GRFUNC_1:31;
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in (i Shift q1) \/ (i Shift q2) or [x,b₁] in i Shift q ) & ( not [x,b₁] in i Shift q or [x,b₁] in (i Shift q1) \/ (i Shift q2) ) )
let y be set ; :: thesis: ( ( not [x,y] in (i Shift q1) \/ (i Shift q2) or [x,y] in i Shift q ) & ( not [x,y] in i Shift q or [x,y] in (i Shift q1) \/ (i Shift q2) ) )
thus ( [x,y] in (i Shift q1) \/ (i Shift q2) implies [x,y] in i Shift q ) :: thesis: ( not [x,y] in i Shift q or [x,y] in (i Shift q1) \/ (i Shift q2) )

proof

assume A8: [x,y] in (i Shift q1) \/ (i Shift q2) ; :: thesis: [x,y] in i Shift q
then ( x in dom q3 & y = q3 . x ) by FUNCT_1:8;
then A9: x in (dom (i Shift q1)) \/ (dom (i Shift q2)) by RELAT_1:13;

A10: now

assume A11: x in dom (i Shift q1) ; :: thesis: ( x in dom (i Shift q) & y = (i Shift q) . x )
then A12: ( dom (i Shift q1) c= dom (i Shift q) & (i Shift q1) . x = (i Shift q) . x ) by A7, GRFUNC_1:8;
then [x,((i Shift q) . x)] in i Shift q1 by A11, FUNCT_1:def 4;
then [x,((i Shift q) . x)] in q3 by XBOOLE_0:def 3;
hence ( x in dom (i Shift q) & y = (i Shift q) . x ) by A8, A11, A12, FUNCT_1:def 1; :: thesis: verum

end;

now

assume A13: x in dom (i Shift q2) ; :: thesis: ( x in dom (i Shift q) & y = (i Shift q) . x )
then A14: ( dom (i Shift q2) c= dom (i Shift q) & (i Shift q2) . x = (i Shift q) . x ) by A7, GRFUNC_1:8;
then [x,((i Shift q) . x)] in i Shift q2 by A13, FUNCT_1:def 4;
then [x,((i Shift q) . x)] in q3 by XBOOLE_0:def 3;
hence ( x in dom (i Shift q) & y = (i Shift q) . x ) by A8, A13, A14, FUNCT_1:def 1; :: thesis: verum

end;

hence [x,y] in i Shift q by A9, A10, FUNCT_1:8, XBOOLE_0:def 3; :: thesis: verum

end;

assume [x,y] in i Shift q ; :: thesis: [x,y] in (i Shift q1) \/ (i Shift q2)
then A15: ( x in dom (i Shift q) & y = (i Shift q) . x ) by FUNCT_1:8;
then consider k being Element of NAT such that
A16: ( x = i + k & k in dom q ) by A3;
dom q = (dom q1) \/ (dom q2) by A1, RELAT_1:13;
then A17: ( k in dom q1 or k in dom q2 ) by A16, XBOOLE_0:def 3;
then ( x in dom (i Shift q1) or x in dom (i Shift q2) ) by A4, A5, A16;
then x in (dom (i Shift q1)) \/ (dom (i Shift q2)) by XBOOLE_0:def 3;
then A18: x in dom q3 by RELAT_1:13;

A19: now

assume A20: x in dom (i Shift q1) ; :: thesis: y = q3 . x
then consider k1 being Element of NAT such that
A21: ( x = i + k1 & k1 in dom q1 ) by A4;
thus y = q . k by A15, A16, Def15
.= q1 . k by A1, A16, A21, GRFUNC_1:35
.= (i Shift q1) . x by A16, A21, Def15
.= q3 . x by A20, GRFUNC_1:35 ; :: thesis: verum

end;

now

assume A22: x in dom (i Shift q2) ; :: thesis: y = q3 . x
then consider k2 being Element of NAT such that
A23: ( x = i + k2 & k2 in dom q2 ) by A5;
thus y = q . k by A15, A16, Def15
.= q2 . k by A1, A16, A23, GRFUNC_1:35
.= (i Shift q2) . x by A16, A23, Def15
.= q3 . x by A22, GRFUNC_1:35 ; :: thesis: verum

end;

hence [x,y] in (i Shift q1) \/ (i Shift q2) by A4, A5, A16, A17, A18, A19, FUNCT_1:8; :: thesis: verum