t " I is Subset of (dom t) by RELAT_1:132;
hence t " I is FinSequence-membered ; :: thesis: verum