let V be RealLinearSpace; :: thesis: for u, v1, v2, w, y 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 u, v1, v2, w, y 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) and
A5: v1 = (b1 * w) + (b2 * y) and
A6: (a1 * b1) + (a2 * b2) = 0 by A2;
consider a19, a29, c1, c2 being Real such that
A7: u = (a19 * w) + (a29 * y) and
A8: v2 = (c1 * w) + (c2 * y) and
A9: (a19 * c1) + (a29 * c2) = 0 by A3;
A10: ( a1 = a19 & a2 = a29 ) by A1, A4, A7, Lm4;
then A11: (a1 * (b1 + c1)) + (a2 * (b2 + c2)) = 0 by A6, A9;
A12: (a1 * (b1 - c1)) + (a2 * (b2 - c2)) = 0 by A6, A9, A10;
v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) by A5, A8, Lm1;
hence u,v1 + v2 are_Ort_wrt w,y by A4, A11; :: thesis: u,v1 - v2 are_Ort_wrt w,y
v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) by A5, A8, Lm1;
hence u,v1 - v2 are_Ort_wrt w,y by A4, A12; :: thesis: verum