let V be RealLinearSpace; :: thesis: for w, y being VECTOR of st Gen w,y holds
for u being VECTOR of ex v being VECTOR of st
( u,v are_Ort_wrt w,y & v <> 0. V )
let w, y be VECTOR of ; :: thesis: ( Gen w,y implies for u being VECTOR of ex v being VECTOR of st
( u,v are_Ort_wrt w,y & v <> 0. V ) )
assume A1: Gen w,y ; :: thesis: for u being VECTOR of ex v being VECTOR of st
( u,v are_Ort_wrt w,y & v <> 0. V )
let u be VECTOR of ; :: thesis: ex v being VECTOR of st
( u,v are_Ort_wrt w,y & v <> 0. V )
consider a1, a2 being Real such that
A2: u = (a1 * w) + (a2 * y) by A1, Def1;

A3: now

set v = (a2 * w) + ((- a1) * y);
assume A4: u <> 0. V ; :: thesis: ex v being Element of the carrier of V st
( u,v are_Ort_wrt w,y & v <> 0. V )
take v = (a2 * w) + ((- a1) * y); :: thesis: ( u,v are_Ort_wrt w,y & v <> 0. V )
(a1 * a2) + (a2 * (- a1)) = 0 ;
hence u,v are_Ort_wrt w,y by A2, Def2; :: thesis: v <> 0. V
v <> 0. V

proof

assume v = 0. V ; :: thesis: contradiction
then ( a2 = 0 & - a1 = 0 ) by A1, Def1;
then u = (0 * w) + (0. V) by A2, RLVECT_1:23
.= 0 * w by RLVECT_1:10
.= 0. V by RLVECT_1:23 ;
hence contradiction by A4; :: thesis: verum

end;

hence v <> 0. V ; :: thesis: verum

end;

now

assume A5: u = 0. V ; :: thesis: ex v being VECTOR of st
( u,v are_Ort_wrt w,y & v <> 0. V )
take v = w; :: thesis: ( u,v are_Ort_wrt w,y & v <> 0. V )
thus u,v are_Ort_wrt w,y by A1, A5, Th9; :: thesis: v <> 0. V
thus v <> 0. V by A1, Lm5; :: thesis: verum

end;

hence ex v being VECTOR of st
( u,v are_Ort_wrt w,y & v <> 0. V ) by A3; :: thesis: verum