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 ;
A1: ( len A = 1 & width A = 1 & len B = 1 & width B = 1 & Indices A = [:(Seg 1),(Seg 1):] & Indices B = [:(Seg 1),(Seg 1):] & len D = 1 & width D = 1 & Indices D = [:(Seg 1),(Seg 1):] ) by MATRIX_1:25;
reconsider C = A * B as Matrix of K ;
A2: Line <*<*a*>*>,1 = <*a*>

proof

A3: len (Line A,1) = width A by MATRIX_1:def 8
.= 1 by MATRIX_1:25 ;
1 in Seg (width A) by A1, FINSEQ_1:4, TARSKI:def 1;
then (Line A,1) . 1 = <*<*a*>*> * 1,1 by MATRIX_1:def 8
.= a by MATRIX_2:5 ;
hence Line <*<*a*>*>,1 = <*a*> by A3, FINSEQ_1:57; :: thesis: verum

end;

A4: Col <*<*b*>*>,1 = <*b*>

proof

A5: len (Col B,1) = len B by MATRIX_1:def 9
.= 1 by MATRIX_1:25 ;
1 in Seg (len B) by A1, FINSEQ_1:4, TARSKI:def 1;
then 1 in dom B by FINSEQ_1:def 3;
then (Col B,1) . 1 = <*<*b*>*> * 1,1 by MATRIX_1:def 9
.= b by MATRIX_2:5 ;
hence Col <*<*b*>*>,1 = <*b*> by A5, FINSEQ_1:57; :: thesis: verum

end;

A6: ( len C = 1 & width C = 1 ) by A1, Def4;
then reconsider C = C as Matrix of 1,K by MATRIX_2:7;
Seg (len C) = dom C by FINSEQ_1:def 3;
then A7: Indices C = [:(Seg 1),(Seg 1):] by A6, MATRIX_1:def 5;

now

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

end;

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