let R be Ring; :: thesis: for i, k, m, n being Nat
for A being Matrix of m,n,R st k in dom A & k in dom (1. (R,n)) holds
(Line (A,i)) "*" (Col ((1. (R,n)),k)) = A * (i,k)
let i, k, m, n be Nat; :: thesis: for A being Matrix of m,n,R st k in dom A & k in dom (1. (R,n)) holds
(Line (A,i)) "*" (Col ((1. (R,n)),k)) = A * (i,k)
let A be Matrix of m,n,R; :: thesis: ( k in dom A & k in dom (1. (R,n)) implies (Line (A,i)) "*" (Col ((1. (R,n)),k)) = A * (i,k) )
assume A1: k in dom A ; :: thesis: ( not k in dom (1. (R,n)) or (Line (A,i)) "*" (Col ((1. (R,n)),k)) = A * (i,k) )
assume A2: k in dom (1. (R,n)) ; :: thesis: (Line (A,i)) "*" (Col ((1. (R,n)),k)) = A * (i,k)

per cases ( m > 0 or m = 0 ) ;

suppose A3: m > 0 ; :: thesis: (Line (A,i)) "*" (Col ((1. (R,n)),k)) = A * (i,k)

set p = Line (A,i);
set q = Col ((1. (R,n)),k);
dom (Line (A,i)) = Seg (len (Line (A,i))) by FINSEQ_1:def 3
.= Seg (width A) by MATRIX_0:def 7 ;
then A4: dom (Line (A,i)) = Seg n by A3, MATRIX_0:23;
dom (1. (R,n)) = Seg (len (1. (R,n))) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24 ;
then A5: k in dom (Line (A,i)) by A2, A4;
dom (1. (R,n)) = Seg (len (Col ((1. (R,n)),k))) by FINSEQ_1:def 3, MATRIX_0:def 8
.= dom (Col ((1. (R,n)),k)) by FINSEQ_1:def 3 ;
then A6: k in dom (Col ((1. (R,n)),k)) by A2;
A7: (Col ((1. (R,n)),k)) . k = 1. R

proof

dom (1. (R,n)) = Seg (len (1. (R,n))) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24 ;
then [k,k] in [:(Seg n),(Seg n):] by A2, ZFMISC_1:87;
then A8: [k,k] in Indices (1. (R,n)) by MATRIX_0:24;
thus (Col ((1. (R,n)),k)) . k = (1. (R,n)) * (k,k) by A2, MATRIX_0:def 8
.= 1. R by A8, MATRIX_1:def 3 ; :: thesis: verum

end;

A9: for k9 being Nat st k9 in dom (Col ((1. (R,n)),k)) & k9 <> k holds
(Col ((1. (R,n)),k)) . k9 = 0. R

proof

let k9 be Nat; :: thesis: ( k9 in dom (Col ((1. (R,n)),k)) & k9 <> k implies (Col ((1. (R,n)),k)) . k9 = 0. R )
assume A10: k9 in dom (Col ((1. (R,n)),k)) ; :: thesis: ( not k9 <> k or (Col ((1. (R,n)),k)) . k9 = 0. R )
assume A11: k9 <> k ; :: thesis: (Col ((1. (R,n)),k)) . k9 = 0. R
A12: dom (1. (R,n)) = Seg (len (1. (R,n))) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24 ;
A13: dom (Col ((1. (R,n)),k)) = Seg (len (Col ((1. (R,n)),k))) by FINSEQ_1:def 3
.= Seg (len (1. (R,n))) by MATRIX_0:def 8
.= Seg n by MATRIX_0:24 ;
[k9,k] in [:(Seg n),(Seg n):] by A2, A10, A12, A13, ZFMISC_1:87;
then [k9,k] in Indices (1. (R,n)) by MATRIX_0:24;
hence 0. R = (1. (R,n)) * (k9,k) by A11, MATRIX_1:def 3
.= (Col ((1. (R,n)),k)) . k9 by A10, A12, A13, MATRIX_0:def 8 ;
:: thesis: verum

end;

k in Seg (width A) by A3, A4, A5, MATRIX_0:23;
then A14: (Line (A,i)) . k = A * (i,k) by MATRIX_0:def 7;
thus (Line (A,i)) "*" (Col ((1. (R,n)),k)) = Sum (mlt ((Line (A,i)),(Col ((1. (R,n)),k)))) by FVSUM_1:def 9
.= A * (i,k) by A5, A6, A7, A9, A14, MATRIX_3:17 ; :: thesis: verum

end;

suppose m = 0 ; :: thesis: (Line (A,i)) "*" (Col ((1. (R,n)),k)) = A * (i,k)

then Seg 0 = Seg (len A) by MATRIX_0:25
.= dom A by FINSEQ_1:def 3 ;
hence (Line (A,i)) "*" (Col ((1. (R,n)),k)) = A * (i,k) by A1; :: thesis: verum

end;

end;