consider a being Point of ;
take Phi a,x ; :: thesis: for a being Point of holds Phi a,x = Phi a,x
thus for a being Point of holds Phi a,x = Phi a,x by Th25; :: thesis: verum