let V be RealLinearSpace; :: thesis: for u, v, v1, v2, w, w1, y being VECTOR of V st Gen w,y & u,v,w1,v1 are_Ort_wrt w,y & u,v,w1,v2 are_Ort_wrt w,y holds
u,v,v1,v2 are_Ort_wrt w,y
let u, v, v1, v2, w, w1, y be VECTOR of V; :: thesis: ( Gen w,y & u,v,w1,v1 are_Ort_wrt w,y & u,v,w1,v2 are_Ort_wrt w,y implies u,v,v1,v2 are_Ort_wrt w,y )
assume that
A1: Gen w,y and
A2: ( u,v,w1,v1 are_Ort_wrt w,y & u,v,w1,v2 are_Ort_wrt w,y ) ; :: thesis: u,v,v1,v2 are_Ort_wrt w,y
( v - u,v1 - w1 are_Ort_wrt w,y & v - u,v2 - w1 are_Ort_wrt w,y ) by A2, ANALMETR:def 3;
then A3: v - u,(v2 - w1) - (v1 - w1) are_Ort_wrt w,y by A1, ANALMETR:10;
(v2 - w1) - (v1 - w1) = v2 - (w1 + (v1 - w1)) by RLVECT_1:27
.= v2 - (v1 - (w1 - w1)) by RLVECT_1:29
.= v2 - (v1 - (0. V)) by RLVECT_1:15
.= v2 - v1 by RLVECT_1:13 ;
hence u,v,v1,v2 are_Ort_wrt w,y by A3, ANALMETR:def 3; :: thesis: verum