let V be RealLinearSpace; :: thesis: for u, u1, v, v1, w, y being VECTOR of V
for p, p1, q, q1 being Element of (AMSpace (V,w,y)) st p = u & p1 = u1 & q = v & q1 = v1 holds
( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y )
let u, u1, v, v1, w, y be VECTOR of V; :: thesis: for p, p1, q, q1 being Element of (AMSpace (V,w,y)) st p = u & p1 = u1 & q = v & q1 = v1 holds
( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y )
let p, p1, q, q1 be Element of (AMSpace (V,w,y)); :: thesis: ( p = u & p1 = u1 & q = v & q1 = v1 implies ( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y ) )
assume A1: ( p = u & p1 = u1 & q = v & q1 = v1 ) ; :: thesis: ( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y )
A2: ( p,q _|_ p1,q1 iff [[p,q],[p1,q1]] in the orthogonality of (AMSpace (V,w,y)) ) by Def6;

hereby :: thesis: ( u,v,u1,v1 are_Ort_wrt w,y implies p,q _|_ p1,q1 )

assume p,q _|_ p1,q1 ; :: thesis: u,v,u1,v1 are_Ort_wrt w,y
then consider u9, v9, u19, v19 being VECTOR of V such that
A3: [u,v] = [u9,v9] and
A4: [u1,v1] = [u19,v19] and
A5: u9,v9,u19,v19 are_Ort_wrt w,y by A1, A2, Def4;
A6: u1 = u19 by A4, ZFMISC_1:27;
( u = u9 & v = v9 ) by A3, ZFMISC_1:27;
hence u,v,u1,v1 are_Ort_wrt w,y by A4, A5, A6, ZFMISC_1:27; :: thesis: verum

end;

assume u,v,u1,v1 are_Ort_wrt w,y ; :: thesis: p,q _|_ p1,q1
hence p,q _|_ p1,q1 by A1, A2, Def4; :: thesis: verum