set a = the Point of RAS;
let y, z be Vector of W; :: thesis: ( ( for a being Point of RAS holds y = Phi (a,x) ) & ( for a being Point of RAS holds z = Phi (a,x) ) implies y = z )
assume that
A1: for a being Point of RAS holds y = Phi (a,x) and
A2: for a being Point of RAS holds z = Phi (a,x) ; :: thesis: y = z
y = Phi ( the Point of RAS,x) by A1;
hence y = z by A2; :: thesis: verum