let u be non zero Element of (TOP-REAL 3); :: thesis: for O being Matrix of 3,REAL
for P being Element of (ProjectiveSpace (TOP-REAL 3))
for p being FinSequence of REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p holds
( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 )
let O be Matrix of 3,REAL; :: thesis: for P being Element of (ProjectiveSpace (TOP-REAL 3))
for p being FinSequence of REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p holds
( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 )
let P be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for p being FinSequence of REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p holds
( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 )
let p be FinSequence of REAL ; :: thesis: ( O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p implies ( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 ) )
assume A1: ( O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p ) ; :: thesis: ( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 )

hereby :: thesis: ( SumAll (QuadraticForm (p,O,p)) = 0 implies P in absolute )

assume P in absolute ; :: thesis: SumAll (QuadraticForm (p,O,p)) = 0
then P in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 } by PASCAL:def 2;
then consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A2: P = Q and
A3: for u being Element of (TOP-REAL 3) st not u is zero & Q = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 ;
consider u1 being Element of (TOP-REAL 3) such that
A4: not u1 is zero and
A5: Q = Dir u1 by ANPROJ_1:26;
reconsider p1 = u1 as FinSequence of REAL by EUCLID:24;
A6: SumAll (QuadraticForm (p1,O,p1)) = qfconic (1,1,(- 1),(2 * 0),(2 * 0),(2 * 0),u1) by A1, PASCAL:13
.= 0 by A3, A4, A5 ;
are_Prop u1,u by A2, A5, A1, A4, ANPROJ_1:22;
then consider a being Real such that
A7: a <> 0 and
A8: u1 = a * u by ANPROJ_1:1;
reconsider fa = a as Element of F_Real by XREAL_0:def 1;
u is Element of REAL 3 by EUCLID:22;
then len p = 3 by A1, EUCLID_8:50;
then SumAll (QuadraticForm (p1,O,p1)) = (fa * fa) * (SumAll (QuadraticForm (p,O,p))) by A1, A8, Th35;
hence SumAll (QuadraticForm (p,O,p)) = 0 by A7, A6; :: thesis: verum

end;

assume SumAll (QuadraticForm (p,O,p)) = 0 ; :: thesis: P in absolute
then 0 = qfconic (1,1,(- 1),(2 * 0),(2 * 0),(2 * 0),u) by A1, PASCAL:13
.= qfconic (1,1,(- 1),0,0,0,u) ;
then for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 by A1, PASCAL:10;
then P in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 } ;
hence P in absolute by PASCAL:def 2; :: thesis: verum