theorem Th26:
for
M being
Matrix of 3,
REAL for
P being
Element of
absolute for
Q being
Element of
real_projective_plane for
u,
v being non
zero Element of
(TOP-REAL 3) for
fp,
fq being
FinSequence of
REAL st
M = symmetric_3 (1,1,
(- 1),
0,
0,
0) &
P = Dir u &
Q = Dir v &
u = fp &
v = fq &
Q in tangent P holds
SumAll (QuadraticForm (fq,M,fp)) = 0