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