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, Th31;
then v - u,v - u are_Ort_wrt w,y by Def3;
then v - u = 0. V by A1, Th15;
hence p = q by RLVECT_1:35; :: thesis: verum