let a, b, c, d, e, f be Real; :: thesis: for u1, u2 being non zero Element of (TOP-REAL 3) st Dir u1 = Dir u2 & qfconic (a,b,c,d,e,f,u1) = 0 holds
qfconic (a,b,c,d,e,f,u2) = 0
let u1, u2 be non zero Element of (TOP-REAL 3); :: thesis: ( Dir u1 = Dir u2 & qfconic (a,b,c,d,e,f,u1) = 0 implies qfconic (a,b,c,d,e,f,u2) = 0 )
assume that
A1: Dir u1 = Dir u2 and
A2: qfconic (a,b,c,d,e,f,u1) = 0 ; :: thesis: qfconic (a,b,c,d,e,f,u2) = 0
are_Prop u1,u2 by A1, ANPROJ_1:22;
then consider r being Real such that
A3: r <> 0 and
A4: u1 = r * u2 by ANPROJ_1:1;
not r is zero by A3;
then A5: r * r <> 0 by ORDINAL1:def 14;
( u1 . 1 = r * (u2 . 1) & u1 . 2 = r * (u2 . 2) & u1 . 3 = r * (u2 . 3) ) by A4, RVSUM_1:44;
then (r * r) * (((((((a * (u2 . 1)) * (u2 . 1)) + ((b * (u2 . 2)) * (u2 . 2))) + ((c * (u2 . 3)) * (u2 . 3))) + ((d * (u2 . 1)) * (u2 . 2))) + ((e * (u2 . 1)) * (u2 . 3))) + ((f * (u2 . 3)) * (u2 . 2))) = (r * r) * 0 by A2;
hence qfconic (a,b,c,d,e,f,u2) = 0 by A5, XCMPLX_1:5; :: thesis: verum