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