let i be Nat; 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; ( 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
; (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 ; RELAT_1:def 2 ( ( 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) )
( 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))
;
[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 ( 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))
;
( 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;
verum end;
now ( 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))
;
( 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;
verum end;
hence
[x,y] in Shift (
q,
i)
by A11, A12, FUNCT_1:1, XBOOLE_0:def 3;
verum
end;
assume A17:
[x,y] in Shift (q,i)
; [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 ( x in dom (Shift (q1,i)) implies y = q3 . x )assume A25:
x in dom (Shift (q1,i))
;
y = q3 . xthen 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
;
verum end;
now ( x in dom (Shift (q2,i)) implies y = q3 . x )assume A27:
x in dom (Shift (q2,i))
;
y = q3 . xthen 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
;
verum end;
hence
[x,y] in (Shift (q1,i)) \/ (Shift (q2,i))
by A4, A5, A20, A22, A23, A24, FUNCT_1:1; verum