let s be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis:
let p, q, r be Element of absolute ; :: thesis:
assume that
A1: p,q,r are_mutually_distinct and
A2: s in (tangent p) /\ (tangent q) ; :: thesis:
reconsider P1 = p, P2 = q, P3 = r, P4 = s as Point of real_projective_plane ;
( P4 in tangent p & P4 in tangent q ) by A2, XBOOLE_0:def 4;
then ( not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear ) by A1, Th27;
then consider N being invertible Matrix of 3,F_Real such that
A3: (homography N) . Dir101 = P1 and
A4: (homography N) . Dirm101 = P2 and
A5: (homography N) . Dir011 = P3 and
A6: (homography N) . Dir010 = P4 by BKMODEL1:44, ANPROJ_9:31;
consider na, nb, nc, nd, ne, nf, ng, nh, ni being Element of F_Real such that
A7: N = <*<*na,nb,nc*>,<*nd,ne,nf*>,<*ng,nh,ni*>*> by PASCAL:3;
reconsider b = - 1 as Element of F_Real by XREAL_0:def 1;
A8: not b is zero ;
reconsider a = 1 as Element of F_Real ;
not a is zero ;
then reconsider a = 1, b = - 1 as non zero Element of F_Real by A8;
reconsider N1 = <*<*a,0,0*>,<*0,a,0*>,<*0,0,b*>*> as invertible Matrix of 3,F_Real by ANPROJ_9:9;
reconsider M = ((N @) * N1) * N as invertible Matrix of 3,F_Real ;
A9: N1 = symmetric_3 (a,a,b,0,0,0) by PASCAL:def 3;
then A10: M is symmetric by PASCAL:7, PASCAL:12;
consider va, vb, vc, vd, ve, vf, vg, vh, vi being Element of F_Real such that
A11: M = <*<*va,vb,vc*>,<*vd,ve,vf*>,<*vg,vh,vi*>*> by PASCAL:3;
A12: ( vb = vd & vc = vg & vh = vf ) by A10, A11, PASCAL:6;
reconsider ra = va, rb = vb, rc = vc, re = ve, rf = vf, ri = vi as Real ;
A13: M = symmetric_3 (ra,re,ri,rb,rc,rf) by A12, A11, PASCAL:def 3;
A14: ( p in conic (1,1,(- 1),0,0,0) & N ~ is invertible ) ;
reconsider NR = MXF2MXR (N ~) as Matrix of 3,REAL by MATRIXR1:def 2;
A15: N1 = symmetric_3 (1,1,(- 1),(0 / 2),(0 / 2),(0 / 2)) by PASCAL:def 3;
reconsider N2 = N1 as Matrix of 3,REAL ;
A16: M = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * N2) * (MXF2MXR ((MXR2MXF NR) ~)) by A15, BKMODEL1:53;
A17: (homography (N ~)) . p = Dir101 by A3, ANPROJ_9:15;
A18: ( ( not ra = 0 or not re = 0 or not ri = 0 or not rb = 0 or not rc = 0 or not rf = 0 ) & (homography (N ~)) . p in conic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf)) ) by A13, A14, A15, A16, PASCAL:16;
Dir101 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 (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),u) = 0 } by A18, A17, PASCAL:def 2;
then consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A19: Dir101 = Q and
A20: for u being Element of (TOP-REAL 3) st not u is zero & Q = Dir u holds
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),u) = 0 ;
( |[1,0,1]| `1 = 1 & |[1,0,1]| `2 = 0 & |[1,0,1]| `3 = 1 ) by EUCLID_5:2;
then A21: ( |[1,0,1]| . 1 = 1 & |[1,0,1]| . 2 = 0 & |[1,0,1]| . 3 = 1 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),|[1,0,1]|) = 0 by A19, A20, BKMODEL1:41;
then A22: 0 = ((((((ra * 1) * 1) + ((re * 0) * 0)) + ((ri * 1) * 1)) + (((2 * rb) * 1) * 0)) + (((2 * rc) * 1) * 1)) + (((2 * rf) * 0) * 1) by A21, PASCAL:def 1
.= (ra + ri) + (2 * rc) ;
A23: (homography (N ~)) . q = Dirm101 by A4, ANPROJ_9:15;
( q in conic (1,1,(- 1),0,0,0) & N ~ is invertible ) ;
then A25: ( ( not ra = 0 or not re = 0 or not ri = 0 or not rb = 0 or not rc = 0 or not rf = 0 ) & (homography (N ~)) . q in conic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf)) ) by A13, PASCAL:16, A15, A16;
Dirm101 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 (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),u) = 0 } by A23, A25, PASCAL:def 2;
then consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A26: Dirm101 = Q and
A27: for u being Element of (TOP-REAL 3) st not u is zero & Q = Dir u holds
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),u) = 0 ;
( |[(- 1),0,1]| `1 = - 1 & |[(- 1),0,1]| `2 = 0 & |[(- 1),0,1]| `3 = 1 ) by EUCLID_5:2;
then A28: ( |[(- 1),0,1]| . 1 = - 1 & |[(- 1),0,1]| . 2 = 0 & |[(- 1),0,1]| . 3 = 1 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),|[(- 1),0,1]|) = 0 by A26, A27, BKMODEL1:41;
then A29: 0 = ((((((ra * (- 1)) * (- 1)) + ((re * 0) * 0)) + ((ri * 1) * 1)) + (((2 * rb) * (- 1)) * 0)) + (((2 * rc) * (- 1)) * 1)) + (((2 * rf) * 0) * 1) by A28, PASCAL:def 1
.= (ra + ri) - (2 * rc) ;
A30: (homography (N ~)) . r = Dir011 by A5, ANPROJ_9:15;
( r in conic (1,1,(- 1),0,0,0) & N ~ is invertible ) ;
then A31: for fa, fb, fc, fe, fi, ff being Real
for N1, M, NR being Matrix of 3,REAL st N1 = symmetric_3 (1,1,(- 1),(0 / 2),(0 / 2),(0 / 2)) & NR = MXF2MXR (N ~) & M = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * N1) * (MXF2MXR ((MXR2MXF NR) ~)) & M = 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 ~)) . r in conic (fa,fe,fi,(2 * fb),(2 * fc),(2 * ff)) ) by PASCAL:16;
( ( not ra = 0 or not re = 0 or not ri = 0 or not rb = 0 or not rc = 0 or not rf = 0 ) & (homography (N ~)) . r in conic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf)) ) by A9, A13, A31, A16;
then Dir011 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 (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),u) = 0 } by A30, PASCAL:def 2;
then consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A32: Dir011 = Q and
A33: for u being Element of (TOP-REAL 3) st not u is zero & Q = Dir u holds
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),u) = 0 ;
( |[0,1,1]| `1 = 0 & |[0,1,1]| `2 = 1 & |[0,1,1]| `3 = 1 ) by EUCLID_5:2;
then A34: ( |[0,1,1]| . 1 = 0 & |[0,1,1]| . 2 = 1 & |[0,1,1]| . 3 = 1 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),|[0,1,1]|) = 0 by A32, A33, BKMODEL1:41;
then A35: 0 = ((((((ra * 0) * 0) + ((re * 1) * 1)) + ((ri * 1) * 1)) + (((2 * rb) * 0) * 1)) + (((2 * rc) * 0) * 1)) + (((2 * rf) * 1) * 1) by A34, PASCAL:def 1
.= (re + ri) + (2 * rf) ;
( rc = 0 & ra = - ri & rb = 0 & rf = 0 & ra = re )

thus rc = 0 by A22, A29; :: thesis:
thus ra = - ri by A22, A29; :: thesis:
consider k1 being Element of (TOP-REAL 3) such that
A36: not k1 is zero and
A37: P1 = Dir k1 by ANPROJ_1:26;
consider k1b being Element of (TOP-REAL 3) such that
A38: not k1b is zero and
A39: P2 = Dir k1b by ANPROJ_1:26;
consider k2 being Element of (TOP-REAL 3) such that
A40: not k2 is zero and
A41: P4 = Dir k2 by ANPROJ_1:26;
reconsider kf1 = k1, kf1b = k1b, kf2 = k2 as FinSequence of REAL by EUCLID:24;
A42: ( P4 in tangent p & N2 is Matrix of 3,REAL & p is Element of absolute & Q is Element of real_projective_plane & k1 is non zero Element of (TOP-REAL 3) & k2 is non zero Element of (TOP-REAL 3) & kf1 is FinSequence of REAL & kf2 is FinSequence of REAL & N2 = symmetric_3 (1,1,(- 1),0,0,0) & p = Dir k1 & P4 = Dir k2 & k1 = kf1 & k2 = kf2 ) by A2, XBOOLE_0:def 4, PASCAL:def 3, A36, A37, A40, A41;
A43: ( P4 in tangent q & N2 is Matrix of 3,REAL & p is Element of absolute & k1b is non zero Element of (TOP-REAL 3) & k2 is non zero Element of (TOP-REAL 3) & kf1b is FinSequence of REAL & kf2 is FinSequence of REAL & N2 = symmetric_3 (1,1,(- 1),0,0,0) & q = Dir k1b & P4 = Dir k2 & k1b = kf1b & k2 = kf2 ) by A2, A38, A40, PASCAL:def 3, A39, A41, XBOOLE_0:def 4;
consider ua, va being Element of (TOP-REAL 3), ufa being FinSequence of F_Real, pa being FinSequence of 1 -tuples_on REAL such that
A44: ( Dir101 = Dir ua & not ua is zero & ua = ufa & pa = N * ufa & va = M2F pa & not va is zero & (homography N) . Dir101 = Dir va ) by ANPROJ_8:def 4;
are_Prop k1,va by A3, A37, A44, ANPROJ_1:22, A36;
then consider li being Real such that
A45: li <> 0 and
A46: k1 = li * va by ANPROJ_1:1;
A47: len (N * (<*ufa*> @)) = len N

ufa in TOP-REAL 3 by A44;
then A48: ufa in REAL 3 by EUCLID:22;
then len ufa = 3 by EUCLID_8:50;
then width <*ufa*> = 3 by ANPROJ_8:75;
then A50: len (<*ufa*> @) = width <*ufa*> by MATRIX_0:29
.= len ufa by MATRIX_0:23 ;
width N = 3 by MATRIX_0:24
.= len (<*ufa*> @) by A50, A48, EUCLID_8:50 ;
hence len (N * (<*ufa*> @)) = len N by MATRIX_3:def 4; :: thesis:

end;

A51: len pa = len N by A47, A44, LAPLACE:def 9
.= 3 by MATRIX_0:23 ;
then A52: kf1 = M2F (li * pa) by A44, A46, ANPROJ_8:83;
consider ub, vb being Element of (TOP-REAL 3), ufb being FinSequence of F_Real, pb being FinSequence of 1 -tuples_on REAL such that
A53: ( Dir010 = Dir ub & not ub is zero & ub = ufb & pb = N * ufb & vb = M2F pb & not vb is zero & (homography N) . Dir010 = Dir vb ) by ANPROJ_8:def 4;
are_Prop ub,|[0,1,0]| by A53, ANPROJ_1:22, ANPROJ_9:def 6, ANPROJ_9:10;
then consider lub being Real such that
A54: lub <> 0 and
A55: ub = lub * |[0,1,0]| by ANPROJ_1:1;
A56: ufb = |[(lub * 0),(lub * 1),(lub * 0)]| by A53, A55, EUCLID_5:8
.= |[0,lub,0]| ;
lub in REAL by XREAL_0:def 1;
then reconsider MUFB = <*ufb*> as Matrix of 1,3,F_Real by A56, BKMODEL1:27;

A57: now :: thesis:

len ufb = 3 by A56, FINSEQ_1:45;
then dom ufb = {1,2,3} by FINSEQ_1:def 3, FINSEQ_3:1;
then ( 1 in dom ufb & 2 in dom ufb & 3 in dom ufb ) by ENUMSET1:def 1;
then ( MUFB * (1,1) = |[0,lub,0]| . 1 & MUFB * (1,2) = |[0,lub,0]| . 2 & MUFB * (1,3) = |[0,lub,0]| . 3 ) by A56, ANPROJ_8:70;
hence ( MUFB * (1,1) = 0 & MUFB * (1,2) = lub & MUFB * (1,3) = 0 ) by FINSEQ_1:45; :: thesis:

end;

are_Prop k2,vb by A41, A6, A53, ANPROJ_1:22, A40;
then consider lj being Real such that
A58: lj <> 0 and
A59: k2 = lj * vb by ANPROJ_1:1;
A60: len (N * (<*ufb*> @)) = len N

proof

ufb in TOP-REAL 3 by A53;
then A61: ufb in REAL 3 by EUCLID:22;
then len ufb = 3 by EUCLID_8:50;
then width <*ufb*> = 3 by ANPROJ_8:75;
then A61bis: len (<*ufb*> @) = width <*ufb*> by MATRIX_0:29
.= len ufb by MATRIX_0:23 ;
width N = 3 by MATRIX_0:24
.= len (<*ufb*> @) by A61, A61bis, EUCLID_8:50 ;
hence len (N * (<*ufb*> @)) = len N by MATRIX_3:def 4; :: thesis:

end;

A62: len pb = len N by A60, A53, LAPLACE:def 9
.= 3 by MATRIX_0:23 ;
then A63: M2F pb is Element of (TOP-REAL 3) by ANPROJ_8:82;
then A64: M2F pb is Element of REAL 3 by EUCLID:22;
then A65: len (M2F pb) = 3 by EUCLID_8:50;
M2F pa is Element of (TOP-REAL 3) by A51, ANPROJ_8:82;
then A66: M2F pa is Element of REAL 3 by EUCLID:22;
then A67: len (M2F pa) = 3 by EUCLID_8:50;
A68: li * (N2 * (M2F pa)) = N2 * (li * (M2F pa))

proof

width N2 = 3 by MATRIX_0:23;
hence li * (N2 * (M2F pa)) = N2 * (li * (M2F pa)) by A67, MATRIXR1:59; :: thesis:

end;

A69: ( len (li * (N2 * (M2F pa))) = 3 & len (N2 * (M2F pa)) = 3 )

proof

ColVec2Mx (M2F pa) = pa by A51, BKMODEL1:33;
then reconsider Mpa = pa as Matrix of REAL ;
A70: len (N2 * (M2F pa)) = len (Col ((N2 * (ColVec2Mx (M2F pa))),1)) by MATRIXR1:def 11
.= len (N2 * (ColVec2Mx (M2F pa))) by MATRIX_0:def 8
.= len (N2 * Mpa) by A51, BKMODEL1:33 ;
reconsider N2F = N2, MpaF = Mpa as Matrix of F_Real ;
A71: width N2F = len Mpa by A51, MATRIX_0:23;
len (N2 * Mpa) = len (N2F * MpaF) by ANPROJ_8:17
.= len N2F by A71, MATRIX_3:def 4
.= 3 by MATRIX_0:23 ;
hence ( len (li * (N2 * (M2F pa))) = 3 & len (N2 * (M2F pa)) = 3 ) by A70, RVSUM_1:117; :: thesis:

end;

then A72: len (M2F pb) = len (N2 * (M2F (li * pa))) by A51, ANPROJ_8:83, A68, A65;
A73: len (M2F pb) = len (N2 * (M2F pa)) by A69, A64, EUCLID_8:50;
A74: kf2 = M2F (lj * pb) by A59, A53, A62, ANPROJ_8:83;
A75: ( len (M2F (lj * pb)) = len N2 & len (M2F (li * pa)) = width N2 & len (M2F (li * pa)) > 0 )

proof

A76: ( len N2 = 3 & width N2 = 3 ) by MATRIX_0:23;
consider p1, p2, p3 being Real such that
A77: ( p1 = (pb . 1) . 1 & p2 = (pb . 2) . 1 & p3 = (pb . 3) . 1 & lj * pb = <*<*(lj * p1)*>,<*(lj * p2)*>,<*(lj * p3)*>*> ) by A62, ANPROJ_8:def 3;
len (lj * pb) = 3 by A77, FINSEQ_1:45;
then A78: M2F (lj * pb) = <*(((lj * pb) . 1) . 1),(((lj * pb) . 2) . 1),(((lj * pb) . 3) . 1)*> by ANPROJ_8:def 2;
consider p1, p2, p3 being Real such that
A79: ( p1 = (pa . 1) . 1 & p2 = (pa . 2) . 1 & p3 = (pa . 3) . 1 & li * pa = <*<*(li * p1)*>,<*(li * p2)*>,<*(li * p3)*>*> ) by A51, ANPROJ_8:def 3;
len (li * pa) = 3 by A79, FINSEQ_1:45;
then M2F (li * pa) = <*(((li * pa) . 1) . 1),(((li * pa) . 2) . 1),(((li * pa) . 3) . 1)*> by ANPROJ_8:def 2;
hence ( len (M2F (lj * pb)) = len N2 & len (M2F (li * pa)) = width N2 & len (M2F (li * pa)) > 0 ) by A76, A78, FINSEQ_1:45; :: thesis:

end;

proof

consider ua2, va2 being Element of (TOP-REAL 3), ufa2 being FinSequence of F_Real, pa2 being FinSequence of 1 -tuples_on REAL such that
A82: ( Dirm101 = Dir ua2 & not ua2 is zero & ua2 = ufa2 & pa2 = N * ufa2 & va2 = M2F pa2 & not va2 is zero & (homography N) . Dirm101 = Dir va2 ) by ANPROJ_8:def 4;
are_Prop k1b,va2 by A39, A4, A82, ANPROJ_1:22, A38;
then consider li2 being Real such that
A83: li2 <> 0 and
A84: k1b = li2 * va2 by ANPROJ_1:1;
A85: len (N * (<*ufa2*> @)) = len N

proof

ufa2 in TOP-REAL 3 by A82;
then A86: ufa2 in REAL 3 by EUCLID:22;
A87: len ufa2 = 3 by A86, EUCLID_8:50;
width <*ufa2*> = 3 by A87, ANPROJ_8:75;
then A88: len (<*ufa2*> @) = width <*ufa2*> by MATRIX_0:29
.= len ufa2 by MATRIX_0:23 ;
width N = 3 by MATRIX_0:24
.= len (<*ufa2*> @) by A88, A86, EUCLID_8:50 ;
hence len (N * (<*ufa2*> @)) = len N by MATRIX_3:def 4; :: thesis:

end;

A89: len pa2 = len N by A85, A82, LAPLACE:def 9
.= 3 by MATRIX_0:23 ;
A90: kf1b = M2F (li2 * pa2) by A82, A84, A89, ANPROJ_8:83;
M2F pa2 is Element of (TOP-REAL 3) by A89, ANPROJ_8:82;
then A91: M2F pa2 is Element of REAL 3 by EUCLID:22;
then A92: len (M2F pa2) = 3 by EUCLID_8:50;
A93: li2 * (N2 * (M2F pa2)) = N2 * (li2 * (M2F pa2))

proof

width N2 = 3 by MATRIX_0:23;
hence li2 * (N2 * (M2F pa2)) = N2 * (li2 * (M2F pa2)) by MATRIXR1:59, A92; :: thesis:

end;

A94: ( len (li2 * (N2 * (M2F pa2))) = 3 & len (N2 * (M2F pa2)) = 3 )

proof

ColVec2Mx (M2F pa2) = pa2 by A89, BKMODEL1:33;
then reconsider Mpa2 = pa2 as Matrix of REAL ;
A95: len (N2 * (M2F pa2)) = len (Col ((N2 * (ColVec2Mx (M2F pa2))),1)) by MATRIXR1:def 11
.= len (N2 * (ColVec2Mx (M2F pa2))) by MATRIX_0:def 8
.= len (N2 * Mpa2) by A89, BKMODEL1:33 ;
reconsider N2F2 = N2, MpaF2 = Mpa2 as Matrix of F_Real ;
A96: width N2F2 = len Mpa2 by A89, MATRIX_0:23;
len (N2 * Mpa2) = len (N2F2 * MpaF2) by ANPROJ_8:17
.= len N2F2 by A96, MATRIX_3:def 4
.= 3 by MATRIX_0:23 ;
hence ( len (li2 * (N2 * (M2F pa2))) = 3 & len (N2 * (M2F pa2)) = 3 ) by A95, RVSUM_1:117; :: thesis:

end;

then A97: len (M2F pb) = len (N2 * (M2F (li2 * pa2))) by A89, ANPROJ_8:83, A93, A65;
A98: len (M2F pb) = len (N2 * (M2F pa2)) by A94, A64, EUCLID_8:50;
A99: kf2 = M2F (lj * pb) by A59, A53, A62, ANPROJ_8:83;
A100: ( len (M2F (lj * pb)) = len N2 & len (M2F (li2 * pa2)) = width N2 & len (M2F (li2 * pa2)) > 0 )

proof

A101: ( len N2 = 3 & width N2 = 3 ) by MATRIX_0:23;
consider p1, p2, p3 being Real such that
A102: ( p1 = (pb . 1) . 1 & p2 = (pb . 2) . 1 & p3 = (pb . 3) . 1 & lj * pb = <*<*(lj * p1)*>,<*(lj * p2)*>,<*(lj * p3)*>*> ) by A62, ANPROJ_8:def 3;
len (lj * pb) = 3 by A102, FINSEQ_1:45;
then A103: M2F (lj * pb) = <*(((lj * pb) . 1) . 1),(((lj * pb) . 2) . 1),(((lj * pb) . 3) . 1)*> by ANPROJ_8:def 2;
consider p1b, p2b, p3b being Real such that
A104: ( p1b = (pa2 . 1) . 1 & p2b = (pa2 . 2) . 1 & p3b = (pa2 . 3) . 1 & li2 * pa2 = <*<*(li2 * p1b)*>,<*(li2 * p2b)*>,<*(li2 * p3b)*>*> ) by A89, ANPROJ_8:def 3;
len (li2 * pa2) = 3 by A104, FINSEQ_1:45;
then M2F (li2 * pa2) = <*(((li2 * pa2) . 1) . 1),(((li2 * pa2) . 2) . 1),(((li2 * pa2) . 3) . 1)*> by ANPROJ_8:def 2;
hence ( len (M2F (lj * pb)) = len N2 & len (M2F (li2 * pa2)) = width N2 & len (M2F (li2 * pa2)) > 0 ) by A101, A103, FINSEQ_1:45; :: thesis:

end;

A105: 0 = SumAll (QuadraticForm ((M2F (lj * pb)),N2,(M2F (li2 * pa2)))) by A43, Th26, A90, A99
.= |((M2F (lj * pb)),(N2 * (M2F (li2 * pa2))))| by A100, MATRPROB:44
.= |((lj * (M2F pb)),(N2 * (M2F (li2 * pa2))))| by A62, ANPROJ_8:83
.= lj * |((M2F pb),(N2 * (M2F (li2 * pa2))))| by A97, RVSUM_1:121
.= lj * |((M2F pb),(li2 * (N2 * (M2F pa2))))| by A93, A89, ANPROJ_8:83
.= lj * (li2 * |((M2F pb),(N2 * (M2F pa2)))|) by A98, RVSUM_1:121
.= (lj * li2) * |((M2F pb),(N2 * (M2F pa2)))| ;
A106: M2F pa2 = <*((pa2 . 1) . 1),((pa2 . 2) . 1),((pa2 . 3) . 1)*> by A89, ANPROJ_8:def 2;
dom (M2F pa2) = Seg 3 by A91, EUCLID_8:50;
then ( (M2F pa2) . 1 in REAL & (M2F pa2) . 2 in REAL & (M2F pa2) . 3 in REAL ) by FINSEQ_1:1, FINSEQ_2:11;
then reconsider s1 = (pa2 . 1) . 1, s2 = (pa2 . 2) . 1, s3 = (pa2 . 3) . 1 as Element of REAL by A106, FINSEQ_1:45;
A107: M2F pb = <*((pb . 1) . 1),((pb . 2) . 1),((pb . 3) . 1)*> by A62, ANPROJ_8:def 2;
dom (M2F pb) = Seg 3 by A64, EUCLID_8:50;
then ( (M2F pb) . 1 in REAL & (M2F pb) . 2 in REAL & (M2F pb) . 3 in REAL ) by FINSEQ_1:1, FINSEQ_2:11;
then reconsider t1 = (pb . 1) . 1, t2 = (pb . 2) . 1, t3 = (pb . 3) . 1 as Element of F_Real by A107, FINSEQ_1:45;
reconsider r1 = 1, r2 = 0 , r3 = - 1 as Element of F_Real by XREAL_0:def 1;
(nb * ((- na) + nc)) + (ne * ((- nd) + nf)) = nh * ((- ng) + ni)

proof

reconsider r1 = 1, r2 = 0 , r3 = - 1 as Element of F_Real by XREAL_0:def 1;
A108: M2F pa2 = <*((pa2 . 1) . 1),((pa2 . 2) . 1),((pa2 . 3) . 1)*> by A89, ANPROJ_8:def 2;
dom (M2F pa2) = Seg 3 by A91, EUCLID_8:50;
then ( (M2F pa2) . 1 in REAL & (M2F pa2) . 2 in REAL & (M2F pa2) . 3 in REAL ) by FINSEQ_1:1, FINSEQ_2:11;
then reconsider s1 = (pa2 . 1) . 1, s2 = (pa2 . 2) . 1, s3 = (pa2 . 3) . 1 as Element of REAL by A108, FINSEQ_1:45;
A109: M2F pb = <*((pb . 1) . 1),((pb . 2) . 1),((pb . 3) . 1)*> by A62, ANPROJ_8:def 2;
dom (M2F pb) = Seg 3 by A64, EUCLID_8:50;
then ( (M2F pb) . 1 in REAL & (M2F pb) . 2 in REAL & (M2F pb) . 3 in REAL ) by FINSEQ_1:1, FINSEQ_2:11;
then reconsider t1 = (pb . 1) . 1, t2 = (pb . 2) . 1, t3 = (pb . 3) . 1 as Element of F_Real by A109, FINSEQ_1:45;
M2F pa2 = <*s1,s2,s3*> by A89, ANPROJ_8:def 2;
then A110: N2 * (M2F pa2) = <*(((1 * s1) + (0 * s2)) + (0 * s3)),(((0 * s1) + (1 * s2)) + (0 * s3)),(((0 * s1) + (0 * s2)) + ((- 1) * s3))*> by PASCAL:9
.= <*s1,s2,(- s3)*> ;
M2F pb = <*t1,t2,t3*> by A62, ANPROJ_8:def 2;
then A111: ( (M2F pb) . 1 = t1 & (M2F pb) . 2 = t2 & (M2F pb) . 3 = t3 & <*s1,s2,(- s3)*> . 1 = s1 & <*s1,s2,(- s3)*> . 2 = s2 & <*s1,s2,(- s3)*> . 3 = - s3 ) by FINSEQ_1:45;
A112: M2F pb is Element of REAL 3 by A63, EUCLID:22;
A113: |[s1,s2,(- s3)]| is Element of REAL 3 by EUCLID:22;
0 = |((M2F pb),<*s1,s2,(- s3)*>)| by A110, A105, A83, A58
.= ((t1 * s1) + (t2 * s2)) + (t3 * (- s3)) by A112, A113, EUCLID_8:63, A111 ;
then A114: (t1 * s1) + (t2 * s2) = t3 * s3 ;
not |[(- 1),0,1]| is zero by EUCLID_5:4, FINSEQ_1:78;
then are_Prop ua2,|[(- 1),0,1]| by A82, ANPROJ_1:22;
then consider lua2 being Real such that
A115: lua2 <> 0 and
A116: ua2 = lua2 * |[(- 1),0,1]| by ANPROJ_1:1;
A117: ua2 = |[(lua2 * (- 1)),(lua2 * 0),(lua2 * 1)]| by A116, EUCLID_5:8
.= |[(- lua2),0,lua2]| ;
reconsider za1 = - lua2, za2 = 0 , za3 = lua2 as Element of F_Real by XREAL_0:def 1;
( lua2 in REAL & - lua2 in REAL ) by XREAL_0:def 1;
then reconsider MUFA = <*ufa2*> as Matrix of 1,3,F_Real by A117, A82, BKMODEL1:27;

now :: thesis:

len ufa2 = 3 by A117, A82, FINSEQ_1:45;
then dom ufa2 = {1,2,3} by FINSEQ_1:def 3, FINSEQ_3:1;
then ( 1 in dom ufa2 & 2 in dom ufa2 & 3 in dom ufa2 ) by ENUMSET1:def 1;
then ( MUFA * (1,1) = |[(- lua2),0,lua2]| . 1 & MUFA * (1,2) = |[(- lua2),0,lua2]| . 2 & MUFA * (1,3) = |[(- lua2),0,lua2]| . 3 ) by A117, A82, ANPROJ_8:70;
hence ( MUFA * (1,1) = - lua2 & MUFA * (1,2) = 0 & MUFA * (1,3) = lua2 ) by FINSEQ_1:45; :: thesis:

end;

then A119: <*ufa2*> @ = <*<*(- lua2)*>,<*0*>,<*lua2*>*> by BKMODEL1:31;
reconsider nlua2 = - lua2 as Element of F_Real by XREAL_0:def 1;
( 0 is Element of F_Real & lua2 is Element of F_Real ) by XREAL_0:def 1;
then reconsider MUFAT = <*<*nlua2*>,<*0*>,<*lua2*>*> as Matrix of 3,1,F_Real by BKMODEL1:28;
A120: N * MUFAT is Matrix of 3,1,F_Real by BKMODEL1:24;
A121: N * ufa2 = N * MUFAT by A119, LAPLACE:def 9;
then N * ufa2 = <*<*((N * ufa2) * (1,1))*>,<*((N * ufa2) * (2,1))*>,<*((N * ufa2) * (3,1))*>*> by A120, BKMODEL1:30;
then A122: ( pa2 . 1 = <*((N * ufa2) * (1,1))*> & pa2 . 2 = <*((N * ufa2) * (2,1))*> & pa2 . 3 = <*((N * ufa2) * (3,1))*> ) by A82, FINSEQ_1:45;
N * MUFAT is Matrix of 3,1,F_Real by BKMODEL1:24;
then A123: Indices (N * MUFAT) = [:(Seg 3),(Seg 1):] by MATRIX_0:23;
width N = 3 by MATRIX_0:24;
then A124: width N = len MUFAT by MATRIX_0:23;
A125: Col (MUFAT,1) = <*za1,za2,za3*> by ANPROJ_8:5;
A126: ( Line (N,1) = <*na,nb,nc*> & Line (N,2) = <*nd,ne,nf*> & Line (N,3) = <*ng,nh,ni*> ) by A7, ANPROJ_9:4;
( (N * MUFAT) * (1,1) = (Line (N,1)) "*" (Col (MUFAT,1)) & (N * MUFAT) * (2,1) = (Line (N,2)) "*" (Col (MUFAT,1)) & (N * MUFAT) * (3,1) = (Line (N,3)) "*" (Col (MUFAT,1)) ) by A123, A124, MATRIX_3:def 4, ANPROJ_8:2;
then ( (N * MUFAT) * (1,1) = ((na * za1) + (nb * za2)) + (nc * za3) & (N * MUFAT) * (2,1) = ((nd * za1) + (ne * za2)) + (nf * za3) & (N * MUFAT) * (3,1) = ((ng * za1) + (nh * za2)) + (ni * za3) ) by A125, A126, ANPROJ_8:7;
then A127: ( (pa2 . 1) . 1 = (na * nlua2) + (nc * lua2) & (pa2 . 2) . 1 = (nd * nlua2) + (nf * lua2) & (pa2 . 3) . 1 = (ng * nlua2) + (ni * lua2) ) by A121, A122, FINSEQ_1:40;
reconsider z1 = 0 , z2 = lub, z3 = 0 as Element of F_Real by XREAL_0:def 1;
( 0 is Element of F_Real & lub is Element of F_Real ) by XREAL_0:def 1;
then reconsider MUFBT = <*<*0*>,<*lub*>,<*0*>*> as Matrix of 3,1,F_Real by BKMODEL1:28;
A128: N * MUFBT is Matrix of 3,1,F_Real by BKMODEL1:24;
A129: N * ufb = N * (<*ufb*> @) by LAPLACE:def 9
.= N * MUFBT by A57, BKMODEL1:31 ;
then N * ufb = <*<*((N * ufb) * (1,1))*>,<*((N * ufb) * (2,1))*>,<*((N * ufb) * (3,1))*>*> by A128, BKMODEL1:30;
then A130: ( pb . 1 = <*((N * ufb) * (1,1))*> & pb . 2 = <*((N * ufb) * (2,1))*> & pb . 3 = <*((N * ufb) * (3,1))*> ) by A53, FINSEQ_1:45;
N * MUFBT is Matrix of 3,1,F_Real by BKMODEL1:24;
then A131: Indices (N * MUFBT) = [:(Seg 3),(Seg 1):] by MATRIX_0:23;
width N = 3 by MATRIX_0:24;
then A132: width N = len MUFBT by MATRIX_0:23;
reconsider z1 = 0 , z2 = lub, z3 = 0 as Element of F_Real by XREAL_0:def 1;
A133: Col (MUFBT,1) = <*z1,z2,z3*> by ANPROJ_8:5;
A134: ( Line (N,1) = <*na,nb,nc*> & Line (N,2) = <*nd,ne,nf*> & Line (N,3) = <*ng,nh,ni*> ) by ANPROJ_9:4, A7;
( (N * MUFBT) * (1,1) = (Line (N,1)) "*" (Col (MUFBT,1)) & (N * MUFBT) * (2,1) = (Line (N,2)) "*" (Col (MUFBT,1)) & (N * MUFBT) * (3,1) = (Line (N,3)) "*" (Col (MUFBT,1)) ) by A132, MATRIX_3:def 4, A131, ANPROJ_8:2;
then ( (N * MUFBT) * (1,1) = ((na * z1) + (nb * z2)) + (nc * z3) & (N * MUFBT) * (2,1) = ((nd * z1) + (ne * z2)) + (nf * z3) & (N * MUFBT) * (3,1) = ((ng * z1) + (nh * z2)) + (ni * z3) ) by A133, A134, ANPROJ_8:7;
then ( (pb . 1) . 1 = nb * lub & (pb . 2) . 1 = ne * lub & (pb . 3) . 1 = nh * lub ) by A129, A130, FINSEQ_1:40;
then ((lua2 * lub) * (nb * ((- na) + nc))) + ((lua2 * lub) * (ne * ((- nd) + nf))) = (lua2 * lub) * (nh * ((- ng) + ni)) by A127, A114;
then (((lua2 * lub) * (nb * ((- na) + nc))) + ((lua2 * lub) * (ne * ((- nd) + nf)))) - ((lua2 * lub) * (nh * ((- ng) + ni))) = 0 ;
then (lua2 * lub) * (((nb * ((- na) + nc)) + (ne * ((- nd) + nf))) - (nh * ((- ng) + ni))) = 0 ;
then ((nb * ((- na) + nc)) + (ne * ((- nd) + nf))) - (nh * ((- ng) + ni)) = 0 by A54, A115;
hence (nb * ((- na) + nc)) + (ne * ((- nd) + nf)) = nh * ((- ng) + ni) ; :: thesis:

end;

hence (nb * ((- na) + nc)) + (ne * ((- nd) + nf)) = nh * ((- ng) + ni) ; :: thesis:

end;

A136: (nb * (na + nc)) + (ne * (nd + nf)) = nh * (ng + ni)

proof

reconsider r1 = 1, r2 = 0 , r3 = - 1 as Element of F_Real by XREAL_0:def 1;
A137: M2F pa = <*((pa . 1) . 1),((pa . 2) . 1),((pa . 3) . 1)*> by A51, ANPROJ_8:def 2;
dom (M2F pa) = Seg 3 by A66, EUCLID_8:50;
then ( (M2F pa) . 1 in REAL & (M2F pa) . 2 in REAL & (M2F pa) . 3 in REAL ) by FINSEQ_1:1, FINSEQ_2:11;
then reconsider s1 = (pa . 1) . 1, s2 = (pa . 2) . 1, s3 = (pa . 3) . 1 as Element of REAL by A137, FINSEQ_1:45;
A138: M2F pb = <*((pb . 1) . 1),((pb . 2) . 1),((pb . 3) . 1)*> by A62, ANPROJ_8:def 2;
dom (M2F pb) = Seg 3 by A64, EUCLID_8:50;
then ( (M2F pb) . 1 in REAL & (M2F pb) . 2 in REAL & (M2F pb) . 3 in REAL ) by FINSEQ_1:1, FINSEQ_2:11;
then reconsider t1 = (pb . 1) . 1, t2 = (pb . 2) . 1, t3 = (pb . 3) . 1 as Element of F_Real by A138, FINSEQ_1:45;
M2F pa = <*s1,s2,s3*> by A51, ANPROJ_8:def 2;
then A139: N2 * (M2F pa) = <*(((1 * s1) + (0 * s2)) + (0 * s3)),(((0 * s1) + (1 * s2)) + (0 * s3)),(((0 * s1) + (0 * s2)) + ((- 1) * s3))*> by PASCAL:9
.= <*s1,s2,(- s3)*> ;
M2F pb = <*t1,t2,t3*> by A62, ANPROJ_8:def 2;
then A140: ( (M2F pb) . 1 = t1 & (M2F pb) . 2 = t2 & (M2F pb) . 3 = t3 & <*s1,s2,(- s3)*> . 1 = s1 & <*s1,s2,(- s3)*> . 2 = s2 & <*s1,s2,(- s3)*> . 3 = - s3 ) by FINSEQ_1:45;
A141: M2F pb is Element of REAL 3 by A63, EUCLID:22;
A142: |[s1,s2,(- s3)]| is Element of REAL 3 by EUCLID:22;
0 = |((M2F pb),<*s1,s2,(- s3)*>)| by A139, A80, A45, A58
.= ((t1 * s1) + (t2 * s2)) + (t3 * (- s3)) by A141, A142, EUCLID_8:63, A140 ;
then A143: (t1 * s1) + (t2 * s2) = t3 * s3 ;
not |[1,0,1]| is zero by EUCLID_5:4, FINSEQ_1:78;
then are_Prop ua,|[1,0,1]| by A44, ANPROJ_1:22;
then consider lua being Real such that
A145: lua <> 0 and
A146: ua = lua * |[1,0,1]| by ANPROJ_1:1;
A147: ua = |[(lua * 1),(lua * 0),(lua * 1)]| by A146, EUCLID_5:8
.= |[lua,0,lua]| ;
reconsider za1 = lua, za2 = 0 , za3 = lua as Element of F_Real by XREAL_0:def 1;
lua in REAL by XREAL_0:def 1;
then reconsider MUFA = <*ufa*> as Matrix of 1,3,F_Real by A147, A44, BKMODEL1:27;

now :: thesis:

len ufa = 3 by A147, A44, FINSEQ_1:45;
then dom ufa = {1,2,3} by FINSEQ_1:def 3, FINSEQ_3:1;
then ( 1 in dom ufa & 2 in dom ufa & 3 in dom ufa ) by ENUMSET1:def 1;
then ( MUFA * (1,1) = |[lua,0,lua]| . 1 & MUFA * (1,2) = |[lua,0,lua]| . 2 & MUFA * (1,3) = |[lua,0,lua]| . 3 ) by A147, A44, ANPROJ_8:70;
hence ( MUFA * (1,1) = lua & MUFA * (1,2) = 0 & MUFA * (1,3) = lua ) by FINSEQ_1:45; :: thesis:

end;

then A148: <*ufa*> @ = <*<*lua*>,<*0*>,<*lua*>*> by BKMODEL1:31;
( 0 is Element of F_Real & lua is Element of F_Real ) by XREAL_0:def 1;
then reconsider MUFAT = <*<*lua*>,<*0*>,<*lua*>*> as Matrix of 3,1,F_Real by BKMODEL1:28;
A149: N * MUFAT is Matrix of 3,1,F_Real by BKMODEL1:24;
A150: N * ufa = N * MUFAT by A148, LAPLACE:def 9;
N * ufa = <*<*((N * ufa) * (1,1))*>,<*((N * ufa) * (2,1))*>,<*((N * ufa) * (3,1))*>*> by A149, A150, BKMODEL1:30;
then ( pa . 1 = <*((N * ufa) * (1,1))*> & pa . 2 = <*((N * ufa) * (2,1))*> & pa . 3 = <*((N * ufa) * (3,1))*> ) by A44, FINSEQ_1:45;
then A152: ( (pa . 1) . 1 = (N * MUFAT) * (1,1) & (pa . 2) . 1 = (N * MUFAT) * (2,1) & (pa . 3) . 1 = (N * MUFAT) * (3,1) ) by A150, FINSEQ_1:40;
N * MUFAT is Matrix of 3,1,F_Real by BKMODEL1:24;
then A153: Indices (N * MUFAT) = [:(Seg 3),(Seg 1):] by MATRIX_0:23;
width N = 3 by MATRIX_0:24;
then A154: width N = len MUFAT by MATRIX_0:23;
A155: Col (MUFAT,1) = <*za1,za2,za3*> by ANPROJ_8:5;
A156: ( Line (N,1) = <*na,nb,nc*> & Line (N,2) = <*nd,ne,nf*> & Line (N,3) = <*ng,nh,ni*> ) by ANPROJ_9:4, A7;
( (N * MUFAT) * (1,1) = (Line (N,1)) "*" (Col (MUFAT,1)) & (N * MUFAT) * (2,1) = (Line (N,2)) "*" (Col (MUFAT,1)) & (N * MUFAT) * (3,1) = (Line (N,3)) "*" (Col (MUFAT,1)) ) by A154, MATRIX_3:def 4, A153, ANPROJ_8:2;
then A157: ( (pa . 1) . 1 = ((na * za1) + (nb * za2)) + (nc * za3) & (pa . 2) . 1 = ((nd * za1) + (ne * za2)) + (nf * za3) & (pa . 3) . 1 = ((ng * za1) + (nh * za2)) + (ni * za3) ) by A152, A155, A156, ANPROJ_8:7;
reconsider z1 = 0 , z2 = lub, z3 = 0 as Element of F_Real by XREAL_0:def 1;
( 0 is Element of F_Real & lub is Element of F_Real ) by XREAL_0:def 1;
then reconsider MUFBT = <*<*0*>,<*lub*>,<*0*>*> as Matrix of 3,1,F_Real by BKMODEL1:28;
A158: N * MUFBT is Matrix of 3,1,F_Real by BKMODEL1:24;
A159: N * ufb = N * (<*ufb*> @) by LAPLACE:def 9
.= N * MUFBT by A57, BKMODEL1:31 ;
N * ufb = <*<*((N * ufb) * (1,1))*>,<*((N * ufb) * (2,1))*>,<*((N * ufb) * (3,1))*>*> by A158, A159, BKMODEL1:30;
then A160: ( pb . 1 = <*((N * ufb) * (1,1))*> & pb . 2 = <*((N * ufb) * (2,1))*> & pb . 3 = <*((N * ufb) * (3,1))*> ) by A53, FINSEQ_1:45;
N * MUFBT is Matrix of 3,1,F_Real by BKMODEL1:24;
then A161: Indices (N * MUFBT) = [:(Seg 3),(Seg 1):] by MATRIX_0:23;
width N = 3 by MATRIX_0:24;
then A162: width N = len MUFBT by MATRIX_0:23;
reconsider z1 = 0 , z2 = lub, z3 = 0 as Element of F_Real by XREAL_0:def 1;
A163: Col (MUFBT,1) = <*z1,z2,z3*> by ANPROJ_8:5;
A164: ( Line (N,1) = <*na,nb,nc*> & Line (N,2) = <*nd,ne,nf*> & Line (N,3) = <*ng,nh,ni*> ) by ANPROJ_9:4, A7;
( (N * MUFBT) * (1,1) = (Line (N,1)) "*" (Col (MUFBT,1)) & (N * MUFBT) * (2,1) = (Line (N,2)) "*" (Col (MUFBT,1)) & (N * MUFBT) * (3,1) = (Line (N,3)) "*" (Col (MUFBT,1)) ) by A162, MATRIX_3:def 4, A161, ANPROJ_8:2;
then ( (N * MUFBT) * (1,1) = ((na * z1) + (nb * z2)) + (nc * z3) & (N * MUFBT) * (2,1) = ((nd * z1) + (ne * z2)) + (nf * z3) & (N * MUFBT) * (3,1) = ((ng * z1) + (nh * z2)) + (ni * z3) ) by A163, A164, ANPROJ_8:7;
then ( (pb . 1) . 1 = nb * lub & (pb . 2) . 1 = ne * lub & (pb . 3) . 1 = nh * lub ) by A160, FINSEQ_1:40, A159;
then ((lua * lub) * (nb * (na + nc))) + ((lua * lub) * (ne * (nd + nf))) = (lua * lub) * (nh * (ng + ni)) by A157, A143;
then (((lua * lub) * (nb * (na + nc))) + ((lua * lub) * (ne * (nd + nf)))) - ((lua * lub) * (nh * (ng + ni))) = 0 ;
then (lua * lub) * (((nb * (na + nc)) + (ne * (nd + nf))) - (nh * (ng + ni))) = 0 ;
then ((nb * (na + nc)) + (ne * (nd + nf))) - (nh * (ng + ni)) = 0 by A54, A145;
hence (nb * (na + nc)) + (ne * (nd + nf)) = nh * (ng + ni) ; :: thesis:

end;

<*<*na,nb,nc*>,<*nd,ne,nf*>,<*ng,nh,ni*>*> = <*<*(N * (1,1)),(N * (1,2)),(N * (1,3))*>,<*(N * (2,1)),(N * (2,2)),(N * (2,3))*>,<*(N * (3,1)),(N * (3,2)),(N * (3,3))*>*> by A7, MATRIXR2:37;
then A166: ( na = N * (1,1) & nb = N * (1,2) & nc = N * (1,3) & nd = N * (2,1) & ne = N * (2,2) & nf = N * (2,3) & ng = N * (3,1) & nh = N * (3,2) & ni = N * (3,3) ) by PASCAL:2;
width N > 0 by MATRIX_0:23;
then ( len N = 3 & len N1 = 3 & width N1 = 3 & width (N @) = len N ) by MATRIX_0:29, MATRIX_0:23;
then A167: <*<*ra,rb,rc*>,<*rb,re,rf*>,<*rc,rf,ri*>*> = (N @) * (N1 * N) by A12, A11, MATRIX_3:33
.= <*<*(((N @) * (N1 * N)) * (1,1)),(((N @) * (N1 * N)) * (1,2)),(((N @) * (N1 * N)) * (1,3))*>,<*(((N @) * (N1 * N)) * (2,1)),(((N @) * (N1 * N)) * (2,2)),(((N @) * (N1 * N)) * (2,3))*>,<*(((N @) * (N1 * N)) * (3,1)),(((N @) * (N1 * N)) * (3,2)),(((N @) * (N1 * N)) * (3,3))*>*> by MATRIXR2:37 ;
A168: ( ((N @) * (N1 * N)) * (1,1) = (((a * (N * (1,1))) * (N * (1,1))) + ((a * (N * (2,1))) * (N * (2,1)))) + ((b * (N * (3,1))) * (N * (3,1))) & ((N @) * (N1 * N)) * (1,2) = (((a * (N * (1,1))) * (N * (1,2))) + ((a * (N * (2,1))) * (N * (2,2)))) + ((b * (N * (3,1))) * (N * (3,2))) & ((N @) * (N1 * N)) * (1,3) = (((a * (N * (1,1))) * (N * (1,3))) + ((a * (N * (2,1))) * (N * (2,3)))) + ((b * (N * (3,1))) * (N * (3,3))) & ((N @) * (N1 * N)) * (2,1) = (((a * (N * (1,2))) * (N * (1,1))) + ((a * (N * (2,2))) * (N * (2,1)))) + ((b * (N * (3,2))) * (N * (3,1))) & ((N @) * (N1 * N)) * (2,2) = (((a * (N * (1,2))) * (N * (1,2))) + ((a * (N * (2,2))) * (N * (2,2)))) + ((b * (N * (3,2))) * (N * (3,2))) & ((N @) * (N1 * N)) * (2,3) = (((a * (N * (1,2))) * (N * (1,3))) + ((a * (N * (2,2))) * (N * (2,3)))) + ((b * (N * (3,2))) * (N * (3,3))) & ((N @) * (N1 * N)) * (3,1) = (((a * (N * (1,3))) * (N * (1,1))) + ((a * (N * (2,3))) * (N * (2,1)))) + ((b * (N * (3,3))) * (N * (3,1))) & ((N @) * (N1 * N)) * (3,2) = (((a * (N * (1,3))) * (N * (1,2))) + ((a * (N * (2,3))) * (N * (2,2)))) + ((b * (N * (3,3))) * (N * (3,2))) & ((N @) * (N1 * N)) * (3,3) = (((a * (N * (1,3))) * (N * (1,3))) + ((a * (N * (2,3))) * (N * (2,3)))) + ((b * (N * (3,3))) * (N * (3,3))) ) by BKMODEL1:23;
A169: ( ra = ((na * na) + (nd * nd)) - (ng * ng) & rb = ((na * nb) + (nd * ne)) - (ng * nh) & rc = ((na * nc) + (nd * nf)) - (ng * ni) & rb = ((na * nb) + (nd * ne)) - (ng * nh) & re = ((nb * nb) + (ne * ne)) - (nh * nh) & rf = ((nb * nc) + (ne * nf)) - (nh * ni) & rc = ((na * nc) + (nd * nf)) - (ng * ni) & rf = ((nb * nc) + (ne * nf)) - (nh * ni) & ri = ((nc * nc) + (nf * nf)) - (ni * ni) ) by A166, A167, PASCAL:2, A168;
A170: (((nb * na) + (nb * nc)) + (ne * nd)) + (ne * nf) = (nh * ng) + (nh * ni) by A136;
(((- (nb * na)) + (nb * nc)) + (- (ne * nd))) + (ne * nf) = (- (nh * ng)) + (nh * ni) by A81;
hence ( rb = 0 & rf = 0 & ra = re ) by A170, A169, A22, A29, A35; :: thesis:

end;

then A170: M = symmetric_3 (ra,ra,(- ra),0,0,0) by A12, A11, PASCAL:def 3;
A171: ra <> 0

proof

assume ra = 0 ; :: thesis:
then Det M = 0. F_Real by A170, BKMODEL1:22;
hence contradiction by LAPLACE:34; :: thesis:

end;

then A172: (homography M) .: absolute = absolute by A170, Th29;
take N ; :: thesis:
thus ( (homography N) .: absolute = absolute & (homography N) . Dir101 = p & (homography N) . Dirm101 = q & (homography N) . Dir011 = r & (homography N) . Dir010 = s ) by A9, A171, A172, A170, A3, A4, A5, A6, BKMODEL1:93; :: thesis: