let p, q, r be Point of (TOP-REAL 3); :: thesis: 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; :: thesis: ( 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*> ; :: thesis: 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; :: thesis: verum