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

proof

A4: dom (Line ((1. (R,m)),i)) = Seg (len (Line ((1. (R,m)),i))) by FINSEQ_1:def 3
.= Seg (width (1. (R,m))) by MATRIX_0:def 7
.= Seg m by MATRIX_0:24 ;
i in Seg (len (1. (R,m))) by A1, FINSEQ_1:def 3;
then A5: i in Seg m by MATRIX_0:24;
hence i in dom (Line ((1. (R,m)),i)) by A4; :: thesis: ( i in dom (Col (A,k)) & (Line ((1. (R,m)),i)) . i = 1. R & ( for k being Nat st k in dom (Line ((1. (R,m)),i)) & k <> i holds
(Line ((1. (R,m)),i)) . k = 0. R ) )
dom (Col (A,k)) = Seg (len (Col (A,k))) by FINSEQ_1:def 3
.= dom A by FINSEQ_1:def 3, MATRIX_0:def 8 ;
hence i in dom (Col (A,k)) by A2; :: thesis: ( (Line ((1. (R,m)),i)) . i = 1. R & ( for k being Nat st k in dom (Line ((1. (R,m)),i)) & k <> i holds
(Line ((1. (R,m)),i)) . k = 0. R ) )
A6: i in Seg (width (1. (R,m))) by A5, MATRIX_0:24;
A7: [i,i] in Indices (1. (R,m))

proof

[i,i] in [:(dom (1. (R,m))),(Seg (width (1. (R,m)))):] by A1, A6, ZFMISC_1:87;
hence [i,i] in Indices (1. (R,m)) by MATRIX_0:def 4; :: thesis: verum

end;

thus (Line ((1. (R,m)),i)) . i = (1. (R,m)) * (i,i) by A6, MATRIX_0:def 7
.= 1. R by A7, MATRIX_1:def 3 ; :: thesis: for k being Nat st k in dom (Line ((1. (R,m)),i)) & k <> i holds
(Line ((1. (R,m)),i)) . k = 0. R
let k be Nat; :: thesis: ( k in dom (Line ((1. (R,m)),i)) & k <> i implies (Line ((1. (R,m)),i)) . k = 0. R )
assume A8: k in dom (Line ((1. (R,m)),i)) ; :: thesis: ( not k <> i or (Line ((1. (R,m)),i)) . k = 0. R )
assume A9: k <> i ; :: thesis: (Line ((1. (R,m)),i)) . k = 0. R
A10: k in Seg (width (1. (R,m))) by A4, A8, MATRIX_0:24;
then [i,k] in [:(dom (1. (R,m))),(Seg (width (1. (R,m)))):] by A1, ZFMISC_1:87;
then A11: [i,k] in Indices (1. (R,m)) by MATRIX_0:def 4;
thus (Line ((1. (R,m)),i)) . k = (1. (R,m)) * (i,k) by A10, MATRIX_0:def 7
.= 0. R by A9, A11, MATRIX_1:def 3 ; :: thesis: verum

end;

thus (Line ((1. (R,m)),i)) "*" (Col (A,k)) = Sum (mlt ((Line ((1. (R,m)),i)),(Col (A,k)))) by FVSUM_1:def 9
.= (Col (A,k)) . i by A3, MATRIX_3:17
.= A * (i,k) by A2, MATRIX_0:def 8 ; :: thesis: verum