let i be Nat; for p, q being FinSubsequence st q c= p holds
Shift (q,i) c= Shift (p,i)
let p, q be FinSubsequence; ( q c= p implies Shift (q,i) c= Shift (p,i) )
assume A1:
q c= p
; Shift (q,i) c= Shift (p,i)
A2:
dom (Shift (q,i)) = { (k + i) where k is Nat : k in dom q }
by Def12;
A3:
dom (Shift (p,i)) = { (k + i) where k is Nat : k in dom p }
by Def12;
let x, y be object ; RELAT_1:def 3 ( not [x,y] in Shift (q,i) or [x,y] in Shift (p,i) )
assume A4:
[x,y] in Shift (q,i)
; [x,y] in Shift (p,i)
then A5:
x in dom (Shift (q,i))
by FUNCT_1:1;
A6:
y = (Shift (q,i)) . x
by A4, FUNCT_1:1;
consider k being Nat such that
A7:
x = k + i
and
A8:
k in dom q
by A2, A5;
A9:
dom q c= dom p
by A1, GRFUNC_1:2;
then A10:
x in dom (Shift (p,i))
by A3, A7, A8;
y =
q . k
by A6, A7, A8, Def12
.=
p . k
by A1, A8, GRFUNC_1:2
.=
(Shift (p,i)) . x
by A7, A8, A9, Def12
;
hence
[x,y] in Shift (p,i)
by A10, FUNCT_1:1; verum