let V be RealLinearSpace; :: thesis: for u, w, y being VECTOR of V st Gen w,y & u,u are_Ort_wrt w,y holds
u = 0. V
let u, w, y be VECTOR of V; :: thesis: ( Gen w,y & u,u are_Ort_wrt w,y implies u = 0. V )

A1: now :: thesis: for a being Real st a <> 0 holds
0 < a * a

let a be Real; :: thesis: ( a <> 0 implies 0 < a * a )
assume A2: a <> 0 ; :: thesis: 0 < a * a
( 0 < a implies 0 < a * a ) by XREAL_1:129;
hence 0 < a * a by A2, XREAL_1:130; :: thesis: verum

end;

assume that
A3: Gen w,y and
A4: u,u are_Ort_wrt w,y ; :: thesis: u = 0. V
consider a1, a2, b1, b2 being Real such that
A5: u = (a1 * w) + (a2 * y) and
A6: u = (b1 * w) + (b2 * y) and
A7: (a1 * b1) + (a2 * b2) = 0 by A4;
A8: ( a1 = b1 & a2 = b2 ) by A3, A5, A6, Lm4;
A9: a2 = 0

proof

assume a2 <> 0 ; :: thesis: contradiction
then 0 < a2 * a2 by A1;
hence contradiction by A7, A8, XREAL_1:29, XREAL_1:63; :: thesis: verum

end;

a1 = 0

proof

assume a1 <> 0 ; :: thesis: contradiction
then 0 < a1 * a1 by A1;
hence contradiction by A7, A8, XREAL_1:29, XREAL_1:63; :: thesis: verum

end;

hence u = (0 * w) + (0. V) by A5, A9, RLVECT_1:10
.= 0 * w by RLVECT_1:4
.= 0. V by RLVECT_1:10 ;
:: thesis: verum