let V be RealLinearSpace; :: thesis: for u1, u2, v, w, y 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 u1, u2, v, w, y 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) and
A6: u1 = (b1 * w) + (b2 * y) and
A7: (a1 * b1) + (a2 * b2) = 0 by A2;
consider a19, a29, c1, c2 being Real such that
A8: v = (a19 * w) + (a29 * y) and
A9: u2 = (c1 * w) + (c2 * y) and
A10: (a19 * c1) + (a29 * c2) = 0 by A3;
A11: a2 = a29 by A1, A5, A8, Lm4;
A12: a1 = a19 by A1, A5, A8, Lm4;

A13: now :: thesis: ( a1 = 0 implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )

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

A19: now :: thesis: ( b1 = 0 implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )

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 A18, RLVECT_1:def 8
.= 0. V by RLVECT_1:10
.= 0 * u2 by RLVECT_1:10 ;
hence ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) ; :: thesis: verum

end;

c1 * u1 = c1 * (b1 * w) by A17, RLVECT_1:4
.= (b1 * c1) * w by RLVECT_1:def 7
.= b1 * u2 by A16, RLVECT_1:def 7 ;
hence ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A19; :: thesis: verum

end;

now :: thesis: ( a1 <> 0 implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )

A20: c2 * (((- a2) * b2) * (a1 ")) = b2 * (((- a2) * c2) * (a1 ")) ;
assume A21: a1 <> 0 ; :: thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
A22: b1 = 1 * b1
.= (a1 * (a1 ")) * b1 by A21, XCMPLX_0:def 7
.= (a1 * b1) * (a1 ")
.= ((- a2) * b2) * (a1 ") by A7 ;
A23: c1 = 1 * c1
.= (a1 * (a1 ")) * c1 by A21, XCMPLX_0:def 7
.= (a1 * c1) * (a1 ")
.= ((- a2) * c2) * (a1 ") by A1, A5, A8, A10, A11, Lm4 ;
then A24: b2 * u2 = ((b2 * (((- a2) * c2) * (a1 "))) * w) + ((b2 * c2) * y) by A9, Lm3;

A25: now :: thesis: ( ( c2 <> 0 or b2 <> 0 ) implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )

assume A26: ( 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 A6, A22, A24, A20, A26, Lm3; :: thesis: verum

end;

now :: thesis: ( b2 = 0 & c2 = 0 implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )

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 A6, A9, A22, A23;
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 A25; :: thesis: verum

end;

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