let V be RealLinearSpace; :: thesis: for w, y, u being VECTOR of V st Gen w,y & u,u are_Ort_wrt w,y holds
u = 0. V
let w, y, u be VECTOR of V; :: thesis: ( Gen w,y & u,u are_Ort_wrt w,y implies u = 0. V )
assume that
A1: Gen w,y and
A2: u,u are_Ort_wrt w,y ; :: thesis: u = 0. V
consider a1, a2, b1, b2 being Real such that
A3: ( u = (a1 * w) + (a2 * y) & u = (b1 * w) + (b2 * y) ) and
A4: (a1 * b1) + (a2 * b2) = 0 by A2, Def2;
A5: ( a1 = b1 & a2 = b2 ) by A1, A3, Lm4;

A6: now

let a be Real; :: thesis: ( a <> 0 implies 0 < a * a )
assume A7: a <> 0 ; :: thesis: 0 < a * a
( 0 < a implies 0 < a * a ) by XREAL_1:131;
hence 0 < a * a by A7, XREAL_1:132; :: thesis: verum

end;

A8: a1 = 0

proof

assume a1 <> 0 ; :: thesis: contradiction
then 0 < a1 * a1 by A6;
hence contradiction by A4, A5, XREAL_1:31, XREAL_1:65; :: thesis: verum

end;

a2 = 0

proof

assume a2 <> 0 ; :: thesis: contradiction
then 0 < a2 * a2 by A6;
hence contradiction by A4, A5, XREAL_1:31, XREAL_1:65; :: thesis: verum

end;

hence u = (0 * w) + (0. V) by A3, A8, RLVECT_1:23
.= 0 * w by RLVECT_1:10
.= 0. V by RLVECT_1:23 ;
:: thesis: verum