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 by A1, XBOOLE_1:7;
A7: q2 c= q by A1, XBOOLE_1:7;
A8: i Shift q1 c= i Shift q by A1, Th70, XBOOLE_1:7;
A9: i Shift q2 c= i Shift q by A1, Th70, XBOOLE_1:7;
dom q1 misses dom q2 by A2, A6, A7, 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:13;
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 A10: [x,y] in (i Shift q1) \/ (i Shift q2) ; :: thesis: [x,y] in i Shift q
then x in dom q3 by FUNCT_1:1;
then A11: x in (dom (i Shift q1)) \/ (dom (i Shift q2)) by RELAT_1:1;

A12: now

assume A13: x in dom (i Shift q1) ; :: thesis: ( x in dom (i Shift q) & y = (i Shift q) . x )
A14: dom (i Shift q1) c= dom (i Shift q) by A8, GRFUNC_1:2;
(i Shift q1) . x = (i Shift q) . x by A8, A13, GRFUNC_1:2;
then [x,((i Shift q) . x)] in i Shift q1 by A13, FUNCT_1:def 2;
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 A10, A13, A14, FUNCT_1:def 1; :: thesis: verum

end;

now

assume A15: x in dom (i Shift q2) ; :: thesis: ( x in dom (i Shift q) & y = (i Shift q) . x )
A16: dom (i Shift q2) c= dom (i Shift q) by A9, GRFUNC_1:2;
(i Shift q2) . x = (i Shift q) . x by A9, A15, GRFUNC_1:2;
then [x,((i Shift q) . x)] in i Shift q2 by A15, FUNCT_1:def 2;
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 A10, A15, A16, FUNCT_1:def 1; :: thesis: verum

end;

hence [x,y] in i Shift q by A11, A12, FUNCT_1:1, XBOOLE_0:def 3; :: thesis: verum

end;

assume A17: [x,y] in i Shift q ; :: thesis: [x,y] in (i Shift q1) \/ (i Shift q2)
then A18: x in dom (i Shift q) by FUNCT_1:1;
A19: y = (i Shift q) . x by A17, FUNCT_1:1;
consider k being Element of NAT such that
A20: x = i + k and
A21: k in dom q by A3, A18;
dom q = (dom q1) \/ (dom q2) by A1, RELAT_1:1;
then A22: ( k in dom q1 or k in dom q2 ) by A21, XBOOLE_0:def 3;
then ( x in dom (i Shift q1) or x in dom (i Shift q2) ) by A4, A5, A20;
then x in (dom (i Shift q1)) \/ (dom (i Shift q2)) by XBOOLE_0:def 3;
then A23: x in dom q3 by RELAT_1:1;

A24: now

assume A25: x in dom (i Shift q1) ; :: thesis: y = q3 . x
then A26: ex k1 being Element of NAT st
( x = i + k1 & k1 in dom q1 ) by A4;
thus y = q . k by A19, A20, A21, Def15
.= q1 . k by A1, A20, A26, GRFUNC_1:15
.= (i Shift q1) . x by A20, A26, Def15
.= q3 . x by A25, GRFUNC_1:15 ; :: thesis: verum

end;

now

assume A27: x in dom (i Shift q2) ; :: thesis: y = q3 . x
then A28: ex k2 being Element of NAT st
( x = i + k2 & k2 in dom q2 ) by A5;
thus y = q . k by A19, A20, A21, Def15
.= q2 . k by A1, A20, A28, GRFUNC_1:15
.= (i Shift q2) . x by A20, A28, Def15
.= q3 . x by A27, GRFUNC_1:15 ; :: thesis: verum

end;

hence [x,y] in (i Shift q1) \/ (i Shift q2) by A4, A5, A20, A22, A23, A24, FUNCT_1:1; :: thesis: verum