let K be Field; for a, b being Element of K holds <*<*a*>*> * <*<*b*>*> = <*<*(a * b)*>*>
let a, b be Element of K; <*<*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 for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = <*<*(a * b)*>*> * (i,j)let i,
j be
Nat;
( [i,j] in Indices C implies C * (i,j) = <*<*(a * b)*>*> * (i,j) )assume A10:
[i,j] in Indices C
;
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
;
verum end;
hence
<*<*a*>*> * <*<*b*>*> = <*<*(a * b)*>*>
by MATRIX_0:27; verum