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 ex k being Element of NAT st
( x = i + k & k in dom q ) by A1;
hence contradiction by A2; :: thesis: verum

end;

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

end;

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

end;

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

now

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

end;

hence q = {} ; :: thesis: verum