x . i is Point of by FUNCOP_1:13;
hence x . i is Element of ; :: thesis: verum