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

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