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 [x,y] in i Shift q ; :: thesis: [x,y] in i Shift p
then A4: ( x in dom (i Shift q) & y = (i Shift q) . x ) by FUNCT_1:8;
then consider k being Element of NAT such that
A5: ( x = i + k & k in dom q ) by A2;
A6: dom q c= dom p by A1, GRFUNC_1:8;
then A7: x in dom (i Shift p) by A3, A5;
y = q . k by A4, A5, Def15
.= p . k by A1, A5, GRFUNC_1:8
.= (i Shift p) . x by A5, A6, Def15 ;
hence [x,y] in i Shift p by A7, FUNCT_1:8; :: thesis: verum