let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u being VECTOR of V ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V )
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u being VECTOR of V ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V ) )
assume A1: Gen w,y ; :: thesis: for u being VECTOR of V ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V )
let u be VECTOR of V; :: thesis: ex v being VECTOR of V 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

assume A4: u = 0. V ; :: thesis: ex v being VECTOR of V 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, A4, Th9; :: thesis: v <> 0. V
thus v <> 0. V by A1, Lm5; :: thesis: verum

end;

now

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

proof

assume (a2 * w) + ((- a1) * y) = 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 A5; :: thesis: verum

end;

A7: (a1 * a2) + (a2 * (- a1)) = 0 ;
take v = (a2 * w) + ((- a1) * y); :: thesis: ( u,v are_Ort_wrt w,y & v <> 0. V )
thus u,v are_Ort_wrt w,y by A2, A7, Def2; :: thesis: v <> 0. V
thus v <> 0. V by A6; :: thesis: verum

end;

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