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