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