(p . a) " I c= dom (p . a) by RELAT_1:132;
hence (p . a) " I is FinSequence-membered ; :: thesis: verum