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