let V be RealLinearSpace; 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; 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)); ( Gen w,y & p,q _|_ p,q implies p = q )
assume that
A1:
Gen w,y
and
A2:
p,q _|_ p,q
; 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; verum