dom f c= A * by RELAT_1:def 18;
hence dom f is FinSequence-membered ; :: thesis: verum