let p, q, r be Point of (TOP-REAL 3); for M being Matrix of 3,F_Real st M = <*p,q,r*> holds
M @ = <*<*(p `1),(q `1),(r `1)*>,<*(p `2),(q `2),(r `2)*>,<*(p `3),(q `3),(r `3)*>*>
let M be Matrix of 3,F_Real; ( M = <*p,q,r*> implies M @ = <*<*(p `1),(q `1),(r `1)*>,<*(p `2),(q `2),(r `2)*>,<*(p `3),(q `3),(r `3)*>*> )
assume A1:
M = <*p,q,r*>
; M @ = <*<*(p `1),(q `1),(r `1)*>,<*(p `2),(q `2),(r `2)*>,<*(p `3),(q `3),(r `3)*>*>
Indices M = [:(Seg 3),(Seg 3):]
by MATRIX_0:24;
then A2:
( (M @) * (1,1) = M * (1,1) & (M @) * (1,2) = M * (2,1) & (M @) * (1,3) = M * (3,1) & (M @) * (2,1) = M * (1,2) & (M @) * (2,2) = M * (2,2) & (M @) * (2,3) = M * (3,2) & (M @) * (3,1) = M * (1,3) & (M @) * (3,2) = M * (2,3) & (M @) * (3,3) = M * (3,3) )
by MATRIX_0:def 6, Th1;
( M * (1,1) = p `1 & M * (2,1) = q `1 & M * (3,1) = r `1 & M * (1,2) = p `2 & M * (2,2) = q `2 & M * (3,2) = r `2 & M * (1,3) = p `3 & M * (2,3) = q `3 & M * (3,3) = r `3 )
by A1, Th18;
hence
M @ = <*<*(p `1),(q `1),(r `1)*>,<*(p `2),(q `2),(r `2)*>,<*(p `3),(q `3),(r `3)*>*>
by A2, MATRIXR2:37; verum