let i be Nat; :: thesis: for q, q1, q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds
(Shift (q1,i)) \/ (Shift (q2,i)) = Shift (q,i)
let q, q1, q2 be FinSubsequence; :: thesis: ( q = q1 \/ q2 & q1 misses q2 implies (Shift (q1,i)) \/ (Shift (q2,i)) = Shift (q,i) )
assume that
A1: q = q1 \/ q2 and
A2: q1 misses q2 ; :: thesis: (Shift (q1,i)) \/ (Shift (q2,i)) = Shift (q,i)
A3: dom (Shift (q,i)) = { (k + i) where k is Nat : k in dom q } by Def12;
A4: dom (Shift (q1,i)) = { (k + i) where k is Nat : k in dom q1 } by Def12;
A5: dom (Shift (q2,i)) = { (k + i) where k is Nat : k in dom q2 } by Def12;
A6: q1 c= q by A1, XBOOLE_1:7;
A7: q2 c= q by A1, XBOOLE_1:7;
A8: Shift (q1,i) c= Shift (q,i) by A1, Th51, XBOOLE_1:7;
A9: Shift (q2,i) c= Shift (q,i) by A1, Th51, XBOOLE_1:7;
dom q1 misses dom q2 by A2, A6, A7, FUNCT_1:112;
then dom (Shift (q1,i)) misses dom (Shift (q2,i)) by Th53;
then reconsider q3 = (Shift (q1,i)) \/ (Shift (q2,i)) as Function by GRFUNC_1:13;
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in (Shift (q1,i)) \/ (Shift (q2,i)) or [x,y] in Shift (q,i) ) & ( not [x,y] in Shift (q,i) or [x,y] in (Shift (q1,i)) \/ (Shift (q2,i)) ) )
thus ( [x,y] in (Shift (q1,i)) \/ (Shift (q2,i)) implies [x,y] in Shift (q,i) ) :: thesis: ( not [x,y] in Shift (q,i) or [x,y] in (Shift (q1,i)) \/ (Shift (q2,i)) )

proof

assume A10: [x,y] in (Shift (q1,i)) \/ (Shift (q2,i)) ; :: thesis: [x,y] in Shift (q,i)
then x in dom q3 by FUNCT_1:1;
then A11: x in (dom (Shift (q1,i))) \/ (dom (Shift (q2,i))) by XTUPLE_0:23;

A12: now :: thesis: ( x in dom (Shift (q1,i)) implies ( x in dom (Shift (q,i)) & y = (Shift (q,i)) . x ) )

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

end;

now :: thesis: ( x in dom (Shift (q2,i)) implies ( x in dom (Shift (q,i)) & y = (Shift (q,i)) . x ) )

assume A15: x in dom (Shift (q2,i)) ; :: thesis: ( x in dom (Shift (q,i)) & y = (Shift (q,i)) . x )
A16: dom (Shift (q2,i)) c= dom (Shift (q,i)) by A9, GRFUNC_1:2;
(Shift (q2,i)) . x = (Shift (q,i)) . x by A9, A15, GRFUNC_1:2;
then [x,((Shift (q,i)) . x)] in Shift (q2,i) by A15, FUNCT_1:def 2;
then [x,((Shift (q,i)) . x)] in q3 by XBOOLE_0:def 3;
hence ( x in dom (Shift (q,i)) & y = (Shift (q,i)) . x ) by A10, A15, A16, FUNCT_1:def 1; :: thesis: verum

end;

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

end;

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

A24: now :: thesis: ( x in dom (Shift (q1,i)) implies y = q3 . x )

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

end;

now :: thesis: ( x in dom (Shift (q2,i)) implies y = q3 . x )

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

end;

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