let a, b, c, d, e, f be Real; 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); ( 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
; 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; verum