let V be RealLinearSpace; :: thesis: for w, y, u, v1, v2 being VECTOR of V st Gen w,y & u,v1 are_Ort_wrt w,y & u,v2 are_Ort_wrt w,y holds
( u,v1 + v2 are_Ort_wrt w,y & u,v1 - v2 are_Ort_wrt w,y )
let w, y, u, v1, v2 be VECTOR of V; :: thesis: ( Gen w,y & u,v1 are_Ort_wrt w,y & u,v2 are_Ort_wrt w,y implies ( u,v1 + v2 are_Ort_wrt w,y & u,v1 - v2 are_Ort_wrt w,y ) )
assume that
A1: Gen w,y and
A2: u,v1 are_Ort_wrt w,y and
A3: u,v2 are_Ort_wrt w,y ; :: thesis: ( u,v1 + v2 are_Ort_wrt w,y & u,v1 - v2 are_Ort_wrt w,y )
consider a1, a2, b1, b2 being Real such that
A4: ( u = (a1 * w) + (a2 * y) & v1 = (b1 * w) + (b2 * y) ) and
A5: (a1 * b1) + (a2 * b2) = 0 by A2, Def2;
consider a1', a2', c1, c2 being Real such that
A6: ( u = (a1' * w) + (a2' * y) & v2 = (c1 * w) + (c2 * y) ) and
A7: (a1' * c1) + (a2' * c2) = 0 by A3, Def2;
A8: ( a1 = a1' & a2 = a2' ) by A1, A4, A6, Lm4;
A9: v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) by A4, A6, Lm1;
(a1 * (b1 + c1)) + (a2 * (b2 + c2)) = 0 by A5, A7, A8;
hence u,v1 + v2 are_Ort_wrt w,y by A4, A9, Def2; :: thesis: u,v1 - v2 are_Ort_wrt w,y
A10: v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) by A4, A6, Lm1;
(a1 * (b1 - c1)) + (a2 * (b2 - c2)) = 0 by A5, A7, A8;
hence u,v1 - v2 are_Ort_wrt w,y by A4, A10, Def2; :: thesis: verum