let q be FinSubsequence; :: thesis: ( q = {} iff Seq q = {} )
thus ( q = {} implies Seq q = {} ) :: thesis: ( Seq q = {} implies q = {} )

proof

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

end;

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