let p be FinSubsequence; :: thesis: ( Seq p = {} implies p = {} )
assume A1: Seq p = {} ; :: thesis: p = {}
( Seq p = p * (Sgm (dom p)) & rng (Sgm (dom p)) = dom p ) by FINSEQ_1:71, FINSEQ_1:def 14;
then dom {} = dom (Sgm (dom p)) by A1, RELAT_1:46;
then Sgm (dom p) = {} ;
then dom p = rng {} by FINSEQ_1:71;
hence p = {} ; :: thesis: verum