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