let i be Element of NAT ; :: thesis: for p, q being FinSubsequence st q c= p holds
i Shift q c= i Shift p
let p, q be FinSubsequence; :: thesis: ( q c= p implies i Shift q c= i Shift p )
assume A1: q c= p ; :: thesis: i Shift q c= i Shift p
A2: dom (i Shift q) = { (i + k) where k is Element of NAT : k in dom q } by Def15;
A3: dom (i Shift p) = { (i + k) where k is Element of NAT : k in dom p } by Def15;
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in i Shift q or [x,b₁] in i Shift p )
let y be set ; :: thesis: ( not [x,y] in i Shift q or [x,y] in i Shift p )
assume A4: [x,y] in i Shift q ; :: thesis: [x,y] in i Shift p
then A5: x in dom (i Shift q) by FUNCT_1:1;
A6: y = (i Shift q) . x by A4, FUNCT_1:1;
consider k being Element of NAT such that
A7: x = i + k 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 (i Shift p) by A3, A7, A8;
y = q . k by A6, A7, A8, Def15
.= p . k by A1, A8, GRFUNC_1:2
.= (i Shift p) . x by A7, A8, A9, Def15 ;
hence [x,y] in i Shift p by A10, FUNCT_1:1; :: thesis: verum