let V be RealLinearSpace; 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; ( 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
; ( 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; 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; verum