let V be RealLinearSpace; :: thesis: for w, y, v, u1, u2 being VECTOR of V st Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v <> 0. V holds
ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
let w, y, v, u1, u2 be VECTOR of V; :: thesis: ( Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v <> 0. V implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )
assume that
A1: Gen w,y and
A2: v,u1 are_Ort_wrt w,y and
A3: v,u2 are_Ort_wrt w,y and
A4: v <> 0. V ; :: thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
consider a1, a2, b1, b2 being Real such that
A5: ( v = (a1 * w) + (a2 * y) & u1 = (b1 * w) + (b2 * y) ) and
A6: (a1 * b1) + (a2 * b2) = 0 by A2, Def2;
consider a1', a2', c1, c2 being Real such that
A7: ( v = (a1' * w) + (a2' * y) & u2 = (c1 * w) + (c2 * y) ) and
A8: (a1' * c1) + (a2' * c2) = 0 by A3, Def2;
A9: ( a1 = a1' & a2 = a2' ) by A1, A5, A7, Lm4;

A10: now

assume A11: a1 = 0 ; :: thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
then A12: a2 <> 0 by A4, A5, Lm2;
then A13: c2 = 0 by A8, A9, A11, XCMPLX_1:6;
b2 = 0 by A6, A11, A12, XCMPLX_1:6;
then A14: ( u1 = (b1 * w) + (0. V) & u2 = (c1 * w) + (0. V) ) by A5, A7, A13, RLVECT_1:23;
then A15: ( u1 = b1 * w & u2 = c1 * w ) by RLVECT_1:10;
A16: c1 * u1 = c1 * (b1 * w) by A14, RLVECT_1:10
.= (b1 * c1) * w by RLVECT_1:def 9
.= b1 * u2 by A15, RLVECT_1:def 9 ;

now

assume b1 = 0 ; :: thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
then 1 * u1 = 0 * w by A15, RLVECT_1:def 9
.= 0. V by RLVECT_1:23
.= 0 * u2 by RLVECT_1:23 ;
hence ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) ; :: thesis: verum

end;

hence ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A16; :: thesis: verum

end;

now

assume A17: a1 <> 0 ; :: thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
A18: b1 = 1 * b1
.= (a1 * (a1 " )) * b1 by A17, XCMPLX_0:def 7
.= (a1 * b1) * (a1 " )
.= ((- a2) * b2) * (a1 " ) by A6 ;
A19: c1 = 1 * c1
.= (a1 * (a1 " )) * c1 by A17, XCMPLX_0:def 7
.= (a1 * c1) * (a1 " )
.= ((- a2) * c2) * (a1 " ) by A8, A9 ;
then A20: b2 * u2 = ((b2 * (((- a2) * c2) * (a1 " ))) * w) + ((b2 * c2) * y) by A7, Lm3;
A21: c2 * (((- a2) * b2) * (a1 " )) = b2 * (((- a2) * c2) * (a1 " )) ;

A22: now

assume A23: ( c2 <> 0 or b2 <> 0 ) ; :: thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
take a = c2; :: thesis: ex b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
take b = b2; :: thesis: ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
thus ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A5, A18, A20, A21, A23, Lm3; :: thesis: verum

end;

now

assume ( b2 = 0 & c2 = 0 ) ; :: thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
then 1 * u1 = 1 * u2 by A5, A7, A18, A19;
hence ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) ; :: thesis: verum

end;

hence ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A22; :: thesis: verum

end;

hence ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A10; :: thesis: verum