let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for p, q being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p,q holds
p = q
let w, y be VECTOR of V; :: thesis: for p, q being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p,q holds
p = q
let p, q be Element of (AMSpace (V,w,y)); :: thesis: ( Gen w,y & p,q _|_ p,q implies p = q )
assume that
A1: Gen w,y and
A2: p,q _|_ p,q ; :: thesis: p = q
reconsider u = p, v = q as Element of V ;
u,v,u,v are_Ort_wrt w,y by A2, Th21;
then v - u,v - u are_Ort_wrt w,y ;
then v - u = 0. V by A1, Th11;
hence p = q by RLVECT_1:21; :: thesis: verum