let K be Field; :: thesis: for a, b being Element of K holds <*<*a*>*> * <*<*b*>*> = <*<*(a * b)*>*>
let a, b be Element of K; :: thesis: <*<*a*>*> * <*<*b*>*> = <*<*(a * b)*>*>
reconsider A = <*<*a*>*> as Matrix of 1,K ;
reconsider B = <*<*b*>*> as Matrix of 1,K ;
reconsider D = <*<*(a * b)*>*> as Matrix of 1,K ;
reconsider C = A * B as Matrix of K ;
A1: len (Line A,1) = width A by MATRIX_1:def 8
.= 1 by MATRIX_1:25 ;
A2: width A = 1 by MATRIX_1:25;
then 1 in Seg (width A) by FINSEQ_1:4, TARSKI:def 1;
then (Line A,1) . 1 = <*<*a*>*> * 1,1 by MATRIX_1:def 8
.= a by MATRIX_2:5 ;
then A3: Line <*<*a*>*>,1 = <*a*> by A1, FINSEQ_1:57;
A4: len B = 1 by MATRIX_1:25;
then 1 in Seg (len B) by FINSEQ_1:4, TARSKI:def 1;
then 1 in dom B by FINSEQ_1:def 3;
then A5: (Col B,1) . 1 = <*<*b*>*> * 1,1 by MATRIX_1:def 9
.= b by MATRIX_2:5 ;
len A = 1 by MATRIX_1:25;
then A6: len C = 1 by A2, A4, Def4;
width B = 1 by MATRIX_1:25;
then A7: width C = 1 by A2, A4, Def4;
then reconsider C = C as Matrix of 1,K by A6, MATRIX_2:7;
Seg (len C) = dom C by FINSEQ_1:def 3;
then A8: Indices C = [:(Seg 1),(Seg 1):] by A6, A7, MATRIX_1:def 5;
len (Col B,1) = len B by MATRIX_1:def 9
.= 1 by MATRIX_1:25 ;
then A9: Col <*<*b*>*>,1 = <*b*> by A5, FINSEQ_1:57;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices C implies C * i,j = <*<*(a * b)*>*> * i,j )
assume A10: [i,j] in Indices C ; :: thesis: C * i,j = <*<*(a * b)*>*> * i,j
then j in Seg 1 by A8, ZFMISC_1:106;
then A11: j = 1 by FINSEQ_1:4, TARSKI:def 1;
i in Seg 1 by A8, A10, ZFMISC_1:106;
then A12: i = 1 by FINSEQ_1:4, TARSKI:def 1;
hence C * i,j = <*a*> "*" <*b*> by A2, A4, A3, A9, A10, A11, Def4
.= a * b by FVSUM_1:113
.= <*<*(a * b)*>*> * i,j by A12, A11, MATRIX_2:5 ;
:: thesis: verum

end;

hence <*<*a*>*> * <*<*b*>*> = <*<*(a * b)*>*> by MATRIX_1:28; :: thesis: verum