let K be Ring; :: 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 C = A * B as Matrix of K ;
A1: len (Line (A,1)) = width A by MATRIX_0:def 7
.= 1 by MATRIX_0:24 ;
A2: width A = 1 by MATRIX_0:24;
then 1 in Seg (width A) by FINSEQ_1:2, TARSKI:def 1;
then (Line (A,1)) . 1 = <*<*a*>*> * (1,1) by MATRIX_0:def 7
.= a by MATRIX_0:49 ;
then A3: Line (<*<*a*>*>,1) = <*a*> by A1, FINSEQ_1:40;
A4: len B = 1 by MATRIX_0:24;
then 1 in Seg (len B) by FINSEQ_1:2, TARSKI:def 1;
then 1 in dom B by FINSEQ_1:def 3;
then A5: (Col (B,1)) . 1 = <*<*b*>*> * (1,1) by MATRIX_0:def 8
.= b by MATRIX_0:49 ;
len A = 1 by MATRIX_0:24;
then A6: len C = 1 by A2, A4, Def4;
width B = 1 by MATRIX_0:24;
then A7: width C = 1 by A2, A4, Def4;
then reconsider C = C as Matrix of 1,K by A6, MATRIX_0:51;
Seg (len C) = dom C by FINSEQ_1:def 3;
then A8: Indices C = [:(Seg 1),(Seg 1):] by A6, A7;
len (Col (B,1)) = len B by MATRIX_0:def 8
.= 1 by MATRIX_0:24 ;
then A9: Col (<*<*b*>*>,1) = <*b*> by A5, FINSEQ_1:40;

now :: thesis: for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = <*<*(a * b)*>*> * (i,j)

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:87;
then A11: j = 1 by FINSEQ_1:2, TARSKI:def 1;
i in Seg 1 by A8, A10, ZFMISC_1:87;
then A12: i = 1 by FINSEQ_1:2, TARSKI:def 1;
hence C * (i,j) = <*a*> "*" <*b*> by A2, A4, A3, A9, A10, A11, Def4
.= a * b by FVSUM_1:88
.= <*<*(a * b)*>*> * (i,j) by A12, A11, MATRIX_0:49 ;
:: thesis: verum

end;

hence <*<*a*>*> * <*<*b*>*> = <*<*(a * b)*>*> by MATRIX_0:27; :: thesis: verum