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: y = (0. V) + y by RLVECT_1:4
.= (0. V) + (1 * y) by RLVECT_1:def 8
.= (0 * w) + (1 * y) by RLVECT_1:10 ;
A2: (1 * 0) + (0 * 1) = 0 ;
w = w + (0. V) by RLVECT_1:4
.= (1 * w) + (0. V) by RLVECT_1:def 8
.= (1 * w) + (0 * y) by RLVECT_1:10 ;
hence w,y are_Ort_wrt w,y by A1, A2; :: thesis: verum