let V be RealLinearSpace; 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; ( 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
; 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; 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;
hence
ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V )
by A3; verum