dom (Re S) = dom S by COMSEQ_3:def 3;
hence Re S is FinSequence-like by Lm1; :: thesis: verum