let p be FinSubsequence; :: thesis: ( Seq p = {} implies p = {} )
assume A1: Seq p = {} ; :: thesis: p = {}
rng (Sgm (dom p)) = dom p by Th50;
then Sgm (dom p) = {} by A1, RELAT_1:27;
then dom p = rng {} by Th50;
hence p = {} ; :: thesis: verum