let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V holds w,y are_Ort_wrt w,y
let w, y be VECTOR of V; :: thesis: w,y are_Ort_wrt w,y
A1: w = w + (0. V) by RLVECT_1:10
.= (1 * w) + (0. V) by RLVECT_1:def 9
.= (1 * w) + (0 * y) by RLVECT_1:23 ;
A2: y = (0. V) + y by RLVECT_1:10
.= (0. V) + (1 * y) by RLVECT_1:def 9
.= (0 * w) + (1 * y) by RLVECT_1:23 ;
(1 * 0 ) + (0 * 1) = 0 ;
hence w,y are_Ort_wrt w,y by A1, A2, Def2; :: thesis: verum