theorem Th16: :: PASCAL:16

for a, b, c, d, e, f being Real
for P being Point of (ProjectiveSpace (TOP-REAL 3))
for N being invertible Matrix of 3,F_Real st ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & P in conic (a,b,c,d,e,f) holds
for fa, fb, fc, fd, fe, fi, ff being Real
for M1, M2, NR being Matrix of 3,REAL st M1 = symmetric_3 (a,b,c,(d / 2),(e / 2),(f / 2)) & NR = MXF2MXR N & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M1) * (MXF2MXR ((MXR2MXF NR) ~)) & M2 = symmetric_3 (fa,fe,fi,fb,fc,ff) holds
( ( not fa = 0 or not fe = 0 or not fi = 0 or not fb = 0 or not ff = 0 or not fc = 0 ) & (homography N) . P in conic (fa,fe,fi,(2 * fb),(2 * fc),(2 * ff)) )