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