consider a being 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 a,x by A1;
hence y = z by A2; :: thesis: verum