let p, q, r be Point of (TOP-REAL 3); :: thesis:
let pf, qf, rf be FinSequence of F_Real; :: thesis:
assume that
A1: p = pf and
A2: q = qf and
A3: r = rf and
A4: |{p,q,r}| <> 0 ; :: thesis:
reconsider pr = p, qr = q, rr = r as Element of REAL 3 by EUCLID:22;
reconsider PQR = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> as Matrix of 3,F_Real by Th16;
len PQR = 3 by MATRIX_0:24;
then A5: dom PQR = Seg 3 by FINSEQ_1:def 3;
then A6: Col ((PQR @),1) = Line (PQR,1) by FINSEQ_1:1, MATRIX_0:58
.= p by Th60 ;
A7: Col ((PQR @),2) = Line (PQR,2) by A5, FINSEQ_1:1, MATRIX_0:58
.= q by Th60 ;
A8: Col ((PQR @),3) = Line (PQR,3) by A5, FINSEQ_1:1, MATRIX_0:58
.= r by Th60 ;
|{p,q,r}| = Det PQR by Th29
.= Det (PQR @) by MATRIXR2:43 ;
then Det (PQR @) <> 0. F_Real by A4, STRUCT_0:def 6;
then consider N being Matrix of 3,F_Real such that
A9: N is_reverse_of PQR @ by LAPLACE:34, MATRIX_6:def 3;
take N ; :: thesis:
thus N is invertible by A9, MATRIX_6:def 3; :: thesis:
( pr in REAL 3 & qr in REAL 3 & rr in REAL 3 ) ;
then A10: ( pr in 3 -tuples_on REAL & qr in 3 -tuples_on REAL & rr in 3 -tuples_on REAL ) by EUCLID:def 1;
then A11: ( len pr = 3 & len qr = 3 & len rr = 3 ) by FINSEQ_2:133;
len (PQR @) = 3 by MATRIX_0:24;
then A12: width N = len (PQR @) by MATRIX_0:24;
A13: dom (N * (PQR @)) = Seg (len (N * (PQR @))) by FINSEQ_1:def 3
.= Seg 3 by MATRIX_0:24 ;
A14: Indices (N * (PQR @)) = [:(Seg 3),(Seg 3):] by MATRIX_0:24;
A15: width <*pf*> = len pf by MATRIX_0:23
.= 3 by A10, A1, FINSEQ_2:133 ;
A16: width <*qf*> = len qf by MATRIX_0:23
.= 3 by A10, A2, FINSEQ_2:133 ;
A17: width <*rf*> = len rf by MATRIX_0:23
.= 3 by A10, A3, FINSEQ_2:133 ;
A18: width N = 3 by MATRIX_0:24
.= len (<*pf*> @) by MATRIX_0:def 6, A15 ;
A19: width N = 3 by MATRIX_0:24
.= len (<*qf*> @) by MATRIX_0:def 6, A16 ;
A20: width N = 3 by MATRIX_0:24
.= len (<*rf*> @) by MATRIX_0:def 6, A17 ;
A21: ( N * pf = N * (<*pf*> @) & N * qf = N * (<*qf*> @) & N * rf = N * (<*rf*> @) ) by LAPLACE:def 9;
A22: len (N * pf) = len (N * (<*pf*> @)) by LAPLACE:def 9
.= len N by A18, MATRIX_3:def 4
.= 3 by MATRIX_0:24 ;
A23: len (N * qf) = len (N * (<*qf*> @)) by LAPLACE:def 9
.= len N by A19, MATRIX_3:def 4
.= 3 by MATRIX_0:24 ;
A24: len (N * rf) = len (N * (<*rf*> @)) by LAPLACE:def 9
.= len N by A20, MATRIX_3:def 4
.= 3 by MATRIX_0:24 ;
( N * (<*pf*> @) is Matrix of 3,1,F_Real & N * (<*qf*> @) is Matrix of 3,1,F_Real & N * (<*rf*> @) is Matrix of 3,1,F_Real ) by A1, A2, A3, A10, Th74, FINSEQ_2:133;
then A25: ( Indices (N * (<*pf*> @)) = [:(Seg 3),(Seg 1):] & Indices (N * (<*qf*> @)) = [:(Seg 3),(Seg 1):] & Indices (N * (<*rf*> @)) = [:(Seg 3),(Seg 1):] ) by MATRIX_0:23;
reconsider CN1 = Col ((N * (PQR @)),1), CN2 = Col ((N * (PQR @)),2), CN3 = Col ((N * (PQR @)),3) as FinSequence of REAL ;
N * (<*pf*> @) = F2M <e1>

proof

N * (<*pf*> @) = F2M CN1

proof

now :: thesis:

A26: dom (N * pf) = Seg 3 by A22, FINSEQ_1:def 3;
A27: len (Col ((N * (PQR @)),1)) = len (Col ((1. (F_Real,3)),1)) by A9, MATRIX_6:def 2
.= len (1. (F_Real,3)) by MATRIX_0:def 8
.= 3 by MATRIX_0:24 ;
then len (F2M CN1) = 3 by Th64;
then dom (F2M CN1) = Seg 3 by FINSEQ_1:def 3;
hence dom (N * (<*pf*> @)) = dom (F2M CN1) by A21, A22, FINSEQ_1:def 3; :: thesis:
thus for x being object st x in dom (N * (<*pf*> @)) holds
(N * (<*pf*> @)) . x = (F2M CN1) . x :: thesis:

proof

let x be object ; :: thesis:
assume A28: x in dom (N * (<*pf*> @)) ; :: thesis:
then reconsider y = x as Nat ;
y in Seg 3 by A28, A26, LAPLACE:def 9;
then not not y = 1 & ... & not y = 3 by FINSEQ_1:91;

per cases ;

suppose A29: y = 1 ; :: thesis:

F2M CN1 = <*<*(CN1 . 1)*>,<*(CN1 . 2)*>,<*(CN1 . 3)*>*> by A27, DEF1;
then A30: (F2M CN1) . 1 = <*(CN1 . 1)*>
.= <*((N * (PQR @)) * (1,1))*> by FINSEQ_1:1, A13, MATRIX_0:def 8 ;
A31: <*((N * (PQR @)) * (1,1))*> = <*((Line (N,1)) "*" (Col ((PQR @),1)))*> by A12, A14, Th1, MATRIX_3:def 4;
A32: ( 1 in Seg 3 & N * (<*pf*> @) is Matrix of 3,1,F_Real ) by FINSEQ_1:1, A10, A1, Th74, FINSEQ_2:133;
Line ((N * (<*pf*> @)),1) = <*((Line (N,1)) "*" (Col ((PQR @),1)))*>

proof

( 1 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
then A33: [1,1] in Indices (N * (<*pf*> @)) by A25, ZFMISC_1:87;
Line ((N * (<*pf*> @)),1) = <*((N * (<*pf*> @)) * (1,1))*> by A11, A1, Th75
.= <*((Line (N,1)) "*" (Col ((<*pf*> @),1)))*> by A18, A33, MATRIX_3:def 4 ;
hence Line ((N * (<*pf*> @)),1) = <*((Line (N,1)) "*" (Col ((PQR @),1)))*> by A1, A6, Th76; :: thesis:

end;

hence (N * (<*pf*> @)) . x = (F2M CN1) . x by A29, A32, MATRIX_0:52, A31, A30; :: thesis:

end;

suppose A34: y = 2 ; :: thesis:

F2M CN1 = <*<*(CN1 . 1)*>,<*(CN1 . 2)*>,<*(CN1 . 3)*>*> by A27, DEF1;
then A35: (F2M CN1) . 2 = <*(CN1 . 2)*>
.= <*((N * (PQR @)) * (2,1))*> by A13, FINSEQ_1:1, MATRIX_0:def 8 ;
A36: <*((N * (PQR @)) * (2,1))*> = <*((Line (N,2)) "*" (Col ((PQR @),1)))*> by A12, MATRIX_3:def 4, A14, Th1;
A37: ( 1 in Seg 3 & N * (<*pf*> @) is Matrix of 3,1,F_Real ) by FINSEQ_1:1, A10, A1, Th74, FINSEQ_2:133;
Line ((N * (<*pf*> @)),2) = <*((Line (N,2)) "*" (Col ((PQR @),1)))*>

proof

( 2 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
then A38: [2,1] in Indices (N * (<*pf*> @)) by A25, ZFMISC_1:87;
Line ((N * (<*pf*> @)),2) = <*((N * (<*pf*> @)) * (2,1))*> by A11, A1, Th75
.= <*((Line (N,2)) "*" (Col ((<*pf*> @),1)))*> by A18, A38, MATRIX_3:def 4 ;
hence Line ((N * (<*pf*> @)),2) = <*((Line (N,2)) "*" (Col ((PQR @),1)))*> by A1, A6, Th76; :: thesis:

end;

hence (N * (<*pf*> @)) . x = (F2M CN1) . x by A34, A37, FINSEQ_1:1, MATRIX_0:52, A36, A35; :: thesis:

end;

suppose A39: y = 3 ; :: thesis:

F2M CN1 = <*<*(CN1 . 1)*>,<*(CN1 . 2)*>,<*(CN1 . 3)*>*> by A27, DEF1;
then A40: (F2M CN1) . 3 = <*(CN1 . 3)*>
.= <*((N * (PQR @)) * (3,1))*> by A13, FINSEQ_1:1, MATRIX_0:def 8 ;
A41: <*((N * (PQR @)) * (3,1))*> = <*((Line (N,3)) "*" (Col ((PQR @),1)))*> by A14, Th1, A12, MATRIX_3:def 4;
A42: ( 1 in Seg 3 & N * (<*pf*> @) is Matrix of 3,1,F_Real ) by FINSEQ_1:1, A10, FINSEQ_2:133, A1, Th74;
Line ((N * (<*pf*> @)),3) = <*((Line (N,3)) "*" (Col ((PQR @),1)))*>

proof

( 3 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
then A43: [3,1] in Indices (N * (<*pf*> @)) by A25, ZFMISC_1:87;
Line ((N * (<*pf*> @)),3) = <*((N * (<*pf*> @)) * (3,1))*> by A1, A11, Th75
.= <*((Line (N,3)) "*" (Col ((<*pf*> @),1)))*> by A18, A43, MATRIX_3:def 4 ;
hence Line ((N * (<*pf*> @)),3) = <*((Line (N,3)) "*" (Col ((PQR @),1)))*> by Th76, A1, A6; :: thesis:

end;

hence (N * (<*pf*> @)) . x = (F2M CN1) . x by A41, A39, A42, FINSEQ_1:1, MATRIX_0:52, A40; :: thesis:

end;

hence N * (<*pf*> @) = F2M CN1 by FUNCT_1:def 11; :: thesis:

end;

hence N * (<*pf*> @) = F2M <e1> by A9, MATRIX_6:def 2, Th55, EUCLID_8:def 1; :: thesis:

end;

hence N * pf = F2M <e1> by LAPLACE:def 9; :: thesis:
N * (<*qf*> @) = F2M <e2>

proof

N * (<*qf*> @) = F2M CN2

proof

now :: thesis:

A44: dom (N * qf) = Seg 3 by A23, FINSEQ_1:def 3;
A45: len (Col ((N * (PQR @)),2)) = len (Col ((1. (F_Real,3)),2)) by A9, MATRIX_6:def 2
.= len (1. (F_Real,3)) by MATRIX_0:def 8
.= 3 by MATRIX_0:24 ;
then len (F2M CN2) = 3 by Th64;
then dom (F2M CN2) = Seg 3 by FINSEQ_1:def 3;
hence dom (N * (<*qf*> @)) = dom (F2M CN2) by A21, A23, FINSEQ_1:def 3; :: thesis:
thus for x being object st x in dom (N * (<*qf*> @)) holds
(N * (<*qf*> @)) . x = (F2M CN2) . x :: thesis:

proof

let x be object ; :: thesis:
assume A46: x in dom (N * (<*qf*> @)) ; :: thesis:
then reconsider y = x as Nat ;
y in Seg 3 by A46, A44, LAPLACE:def 9;
then not not y = 1 & ... & not y = 3 by FINSEQ_1:91;

per cases ;

suppose A47: y = 1 ; :: thesis:

F2M CN2 = <*<*(CN2 . 1)*>,<*(CN2 . 2)*>,<*(CN2 . 3)*>*> by A45, DEF1;
then A48: (F2M CN2) . 1 = <*(CN2 . 1)*>
.= <*((N * (PQR @)) * (1,2))*> by FINSEQ_1:1, A13, MATRIX_0:def 8 ;
A49: <*((N * (PQR @)) * (1,2))*> = <*((Line (N,1)) "*" (Col ((PQR @),2)))*> by A12, A14, Th1, MATRIX_3:def 4;
A50: ( 1 in Seg 3 & N * (<*qf*> @) is Matrix of 3,1,F_Real ) by FINSEQ_1:1, A10, A2, Th74, FINSEQ_2:133;
Line ((N * (<*qf*> @)),1) = <*((Line (N,1)) "*" (Col ((PQR @),2)))*>

proof

( 1 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
then A51: [1,1] in Indices (N * (<*qf*> @)) by A25, ZFMISC_1:87;
Line ((N * (<*qf*> @)),1) = <*((N * (<*qf*> @)) * (1,1))*> by A11, A2, Th75
.= <*((Line (N,1)) "*" (Col ((<*qf*> @),1)))*> by A19, A51, MATRIX_3:def 4 ;
hence Line ((N * (<*qf*> @)),1) = <*((Line (N,1)) "*" (Col ((PQR @),2)))*> by A2, A7, Th76; :: thesis:

end;

hence (N * (<*qf*> @)) . x = (F2M CN2) . x by A47, A50, MATRIX_0:52, A49, A48; :: thesis:

end;

suppose A52: y = 2 ; :: thesis:

F2M CN2 = <*<*(CN2 . 1)*>,<*(CN2 . 2)*>,<*(CN2 . 3)*>*> by A45, DEF1;
then A53: (F2M CN2) . 2 = <*(CN2 . 2)*>
.= <*((N * (PQR @)) * (2,2))*> by A13, FINSEQ_1:1, MATRIX_0:def 8 ;
A54: <*((N * (PQR @)) * (2,2))*> = <*((Line (N,2)) "*" (Col ((PQR @),2)))*> by A12, MATRIX_3:def 4, A14, Th1;
A55: ( 2 in Seg 3 & N * (<*qf*> @) is Matrix of 3,1,F_Real ) by FINSEQ_1:1, A10, A2, Th74, FINSEQ_2:133;
Line ((N * (<*qf*> @)),2) = <*((Line (N,2)) "*" (Col ((PQR @),2)))*>

proof

( 2 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
then A56: [2,1] in Indices (N * (<*qf*> @)) by A25, ZFMISC_1:87;
Line ((N * (<*qf*> @)),2) = <*((N * (<*qf*> @)) * (2,1))*> by A11, A2, Th75
.= <*((Line (N,2)) "*" (Col ((<*qf*> @),1)))*> by A19, A56, MATRIX_3:def 4 ;
hence Line ((N * (<*qf*> @)),2) = <*((Line (N,2)) "*" (Col ((PQR @),2)))*> by A2, A7, Th76; :: thesis:

end;

hence (N * (<*qf*> @)) . x = (F2M CN2) . x by A52, A55, MATRIX_0:52, A54, A53; :: thesis:

end;

suppose A57: y = 3 ; :: thesis:

F2M CN2 = <*<*(CN2 . 1)*>,<*(CN2 . 2)*>,<*(CN2 . 3)*>*> by A45, DEF1;
then A58: (F2M CN2) . 3 = <*(CN2 . 3)*>
.= <*((N * (PQR @)) * (3,2))*> by A13, FINSEQ_1:1, MATRIX_0:def 8 ;
A59: <*((N * (PQR @)) * (3,2))*> = <*((Line (N,3)) "*" (Col ((PQR @),2)))*> by A14, Th1, A12, MATRIX_3:def 4;
A60: ( 3 in Seg 3 & N * (<*qf*> @) is Matrix of 3,1,F_Real ) by FINSEQ_1:1, A10, FINSEQ_2:133, A2, Th74;
Line ((N * (<*qf*> @)),3) = <*((Line (N,3)) "*" (Col ((PQR @),2)))*>

proof

( 3 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
then A61: [3,1] in Indices (N * (<*qf*> @)) by A25, ZFMISC_1:87;
Line ((N * (<*qf*> @)),3) = <*((N * (<*qf*> @)) * (3,1))*> by A2, A11, Th75
.= <*((Line (N,3)) "*" (Col ((<*qf*> @),1)))*> by A19, A61, MATRIX_3:def 4 ;
hence Line ((N * (<*qf*> @)),3) = <*((Line (N,3)) "*" (Col ((PQR @),2)))*> by Th76, A2, A7; :: thesis:

end;

hence (N * (<*qf*> @)) . x = (F2M CN2) . x by A59, A57, A60, MATRIX_0:52, A58; :: thesis:

end;

hence N * (<*qf*> @) = F2M CN2 by FUNCT_1:def 11; :: thesis:

end;

hence N * (<*qf*> @) = F2M <e2> by A9, MATRIX_6:def 2, Th55, EUCLID_8:def 2; :: thesis:

end;

hence N * qf = F2M <e2> by LAPLACE:def 9; :: thesis:
N * (<*rf*> @) = F2M <e3>

proof

N * (<*rf*> @) = F2M CN3

proof

now :: thesis:

A62: dom (N * rf) = Seg 3 by A24, FINSEQ_1:def 3;
A63: len (Col ((N * (PQR @)),3)) = len (Col ((1. (F_Real,3)),3)) by A9, MATRIX_6:def 2
.= len (1. (F_Real,3)) by MATRIX_0:def 8
.= 3 by MATRIX_0:24 ;
len (F2M CN3) = 3 by A63, Th64;
then dom (F2M CN3) = Seg 3 by FINSEQ_1:def 3;
hence dom (N * (<*rf*> @)) = dom (F2M CN3) by A21, A24, FINSEQ_1:def 3; :: thesis:
thus for x being object st x in dom (N * (<*rf*> @)) holds
(N * (<*rf*> @)) . x = (F2M CN3) . x :: thesis:

proof

let x be object ; :: thesis:
assume A64: x in dom (N * (<*rf*> @)) ; :: thesis:
then reconsider y = x as Nat ;
y in Seg 3 by A64, A62, LAPLACE:def 9;
then not not y = 1 & ... & not y = 3 by FINSEQ_1:91;

per cases ;

suppose A65: y = 1 ; :: thesis:

F2M CN3 = <*<*(CN3 . 1)*>,<*(CN3 . 2)*>,<*(CN3 . 3)*>*> by A63, DEF1;
then A66: (F2M CN3) . 1 = <*(CN3 . 1)*>
.= <*((N * (PQR @)) * (1,3))*> by FINSEQ_1:1, A13, MATRIX_0:def 8 ;
A67: <*((N * (PQR @)) * (1,3))*> = <*((Line (N,1)) "*" (Col ((PQR @),3)))*> by A12, A14, Th1, MATRIX_3:def 4;
A68: ( 1 in Seg 3 & N * (<*rf*> @) is Matrix of 3,1,F_Real ) by FINSEQ_1:1, A10, A3, Th74, FINSEQ_2:133;
Line ((N * (<*rf*> @)),1) = <*((Line (N,1)) "*" (Col ((PQR @),3)))*>

proof

( 1 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
then A69: [1,1] in Indices (N * (<*rf*> @)) by A25, ZFMISC_1:87;
Line ((N * (<*rf*> @)),1) = <*((N * (<*rf*> @)) * (1,1))*> by A11, A3, Th75
.= <*((Line (N,1)) "*" (Col ((<*rf*> @),1)))*> by A20, A69, MATRIX_3:def 4 ;
hence Line ((N * (<*rf*> @)),1) = <*((Line (N,1)) "*" (Col ((PQR @),3)))*> by A3, A8, Th76; :: thesis:

end;

hence (N * (<*rf*> @)) . x = (F2M CN3) . x by A65, A68, MATRIX_0:52, A67, A66; :: thesis:

end;

suppose A70: y = 2 ; :: thesis:

F2M CN3 = <*<*(CN3 . 1)*>,<*(CN3 . 2)*>,<*(CN3 . 3)*>*> by A63, DEF1;
then A71: (F2M CN3) . 2 = <*(CN3 . 2)*>
.= <*((N * (PQR @)) * (2,3))*> by A13, FINSEQ_1:1, MATRIX_0:def 8 ;
A72: <*((N * (PQR @)) * (2,3))*> = <*((Line (N,2)) "*" (Col ((PQR @),3)))*> by A12, MATRIX_3:def 4, A14, Th1;
A73: ( 1 in Seg 3 & N * (<*rf*> @) is Matrix of 3,1,F_Real ) by FINSEQ_1:1, A10, A3, Th74, FINSEQ_2:133;
Line ((N * (<*rf*> @)),2) = <*((Line (N,2)) "*" (Col ((PQR @),3)))*>

proof

( 2 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
then A74: [2,1] in Indices (N * (<*rf*> @)) by A25, ZFMISC_1:87;
Line ((N * (<*rf*> @)),2) = <*((N * (<*rf*> @)) * (2,1))*> by A11, A3, Th75
.= <*((Line (N,2)) "*" (Col ((<*rf*> @),1)))*> by A20, A74, MATRIX_3:def 4 ;
hence Line ((N * (<*rf*> @)),2) = <*((Line (N,2)) "*" (Col ((PQR @),3)))*> by A3, A8, Th76; :: thesis:

end;

hence (N * (<*rf*> @)) . x = (F2M CN3) . x by A70, A73, FINSEQ_1:1, MATRIX_0:52, A72, A71; :: thesis:

end;

suppose A75: y = 3 ; :: thesis:

F2M CN3 = <*<*(CN3 . 1)*>,<*(CN3 . 2)*>,<*(CN3 . 3)*>*> by A63, DEF1;
then A76: (F2M CN3) . 3 = <*(CN3 . 3)*>
.= <*((N * (PQR @)) * (3,3))*> by A13, FINSEQ_1:1, MATRIX_0:def 8 ;
A77: <*((N * (PQR @)) * (3,3))*> = <*((Line (N,3)) "*" (Col ((PQR @),3)))*> by A14, Th1, A12, MATRIX_3:def 4;
A78: ( 3 in Seg 3 & N * (<*rf*> @) is Matrix of 3,1,F_Real ) by FINSEQ_1:1, A10, FINSEQ_2:133, A3, Th74;
Line ((N * (<*rf*> @)),3) = <*((Line (N,3)) "*" (Col ((PQR @),3)))*>

proof

( 3 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
then A79: [3,1] in Indices (N * (<*rf*> @)) by A25, ZFMISC_1:87;
Line ((N * (<*rf*> @)),3) = <*((N * (<*rf*> @)) * (3,1))*> by A3, A11, Th75
.= <*((Line (N,3)) "*" (Col ((<*rf*> @),1)))*> by A20, A79, MATRIX_3:def 4 ;
hence Line ((N * (<*rf*> @)),3) = <*((Line (N,3)) "*" (Col ((PQR @),3)))*> by Th76, A3, A8; :: thesis:

end;

hence (N * (<*rf*> @)) . x = (F2M CN3) . x by A77, A75, A78, MATRIX_0:52, A76; :: thesis:

end;

hence N * (<*rf*> @) = F2M CN3 by FUNCT_1:def 11; :: thesis:

end;

hence N * (<*rf*> @) = F2M <e3> by A9, MATRIX_6:def 2, Th55, EUCLID_8:def 3; :: thesis:

end;

hence N * rf = F2M <e3> by LAPLACE:def 9; :: thesis: