let i be Element of NAT ; :: thesis: for q being FinSubsequence holds
( q = {} iff i Shift q = {} )
let q be FinSubsequence; :: thesis: ( q = {} iff i Shift q = {} )
A1: dom (i Shift q) = { (i + k) where k is Element of NAT : k in dom q } by Def15;
thus ( q = {} implies i Shift q = {} ) :: thesis: ( i Shift q = {} implies q = {} )

proof

assume A2: q = {} ; :: thesis: i Shift q = {}

now

let x, y be set ; :: thesis: not [x,y] in i Shift q

now

assume x in dom (i Shift q) ; :: thesis: contradiction
then consider k being Element of NAT such that
A5: ( x = i + k & k in dom q ) by A1;
thus contradiction by A2, A5; :: thesis: verum

end;

hence not [x,y] in i Shift q by FUNCT_1:8; :: thesis: verum

end;

hence i Shift q = {} by RELAT_1:56; :: thesis: verum

end;

assume A6: i Shift q = {} ; :: thesis: q = {}

now

assume q <> {} ; :: thesis: contradiction
then consider x being set such that
A7: x in dom q by XBOOLE_0:def 1;
A8: x in rng (Sgm (dom q)) by A7, FINSEQ_1:71;
rng (Sgm (dom q)) c= NAT by FINSEQ_1:def 4;
then reconsider x = x as Element of NAT by A8;
consider k being Element of NAT such that
A9: ( k = i + x & x in dom q ) by A7;
k in dom (i Shift q) by A1, A9;
hence contradiction by A6; :: thesis: verum

end;

hence q = {} ; :: thesis: verum