let i be Element of NAT ; :: thesis: for p, q being FinSubsequence st q c= p holds
dom (i Shift q) c= dom (i Shift p)
let p, q be FinSubsequence; :: thesis: ( q c= p implies dom (i Shift q) c= dom (i Shift p) )
assume A1: q c= p ; :: thesis: dom (i Shift q) c= dom (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;
A4: dom q c= dom p by A1, GRFUNC_1:2;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (i Shift q) or x in dom (i Shift p) )
assume x in dom (i Shift q) ; :: thesis: x in dom (i Shift p)
then ex k1 being Element of NAT st
( x = i + k1 & k1 in dom q ) by A2;
hence x in dom (i Shift p) by A3, A4; :: thesis: verum