let q be FinSubsequence; :: thesis: ( q = {} iff Seq q = {} )
consider k being Nat such that
A1: dom q c= Seg k by FINSEQ_1:def 12;
thus ( q = {} implies Seq q = {} ) :: thesis: ( Seq q = {} implies q = {} )

proof

assume A2: q = {} ; :: thesis: Seq q = {}
A3: Seq q = q * (Sgm (dom q)) by FINSEQ_1:def 14;
dom q = {} by A2;
hence Seq q = q * {} by A1, A3, FINSEQ_1:72
.= {} ;
:: thesis: verum

end;

thus ( Seq q = {} implies q = {} ) by Lm1; :: thesis: verum