let R be Ring; :: thesis: for i, k, m, n being Nat
for A being Matrix of m,n,R st k in dom (0. (R,n)) holds
(Line (A,i)) "*" (Col ((0. (R,n)),k)) = 0. R
let i, k, m, n be Nat; :: thesis: for A being Matrix of m,n,R st k in dom (0. (R,n)) holds
(Line (A,i)) "*" (Col ((0. (R,n)),k)) = 0. R
let A be Matrix of m,n,R; :: thesis: ( k in dom (0. (R,n)) implies (Line (A,i)) "*" (Col ((0. (R,n)),k)) = 0. R )
assume A1: k in dom (0. (R,n)) ; :: thesis: (Line (A,i)) "*" (Col ((0. (R,n)),k)) = 0. R
set p = mlt ((Line (A,i)),(Col ((0. (R,n)),k)));
A2: for i9 being Element of NAT st i9 in dom (mlt ((Line (A,i)),(Col ((0. (R,n)),k)))) holds
(mlt ((Line (A,i)),(Col ((0. (R,n)),k)))) . i9 = 0. R

proof

let i9 be Element of NAT ; :: thesis: ( i9 in dom (mlt ((Line (A,i)),(Col ((0. (R,n)),k)))) implies (mlt ((Line (A,i)),(Col ((0. (R,n)),k)))) . i9 = 0. R )
assume A3: i9 in dom (mlt ((Line (A,i)),(Col ((0. (R,n)),k)))) ; :: thesis: (mlt ((Line (A,i)),(Col ((0. (R,n)),k)))) . i9 = 0. R

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

suppose A4: m > 0 ; :: thesis: (mlt ((Line (A,i)),(Col ((0. (R,n)),k)))) . i9 = 0. R

A5: len (Line (A,i)) = width A by MATRIX_0:def 7
.= n by A4, MATRIX_0:23
.= len (0. (R,n)) by MATRIX_0:25
.= len (Col ((0. (R,n)),k)) by MATRIX_0:def 8 ;
A6: i9 in Seg (width A)

proof

i9 in Seg (len (mlt ((Line (A,i)),(Col ((0. (R,n)),k))))) by A3, FINSEQ_1:def 3;
then i9 in Seg (min ((len (Line (A,i))),(len (Col ((0. (R,n)),k))))) by MATRIX_3:13;
hence i9 in Seg (width A) by A5, MATRIX_0:def 7; :: thesis: verum

end;

then A7: (Line (A,i)) . i9 = A * (i,i9) by MATRIX_0:def 7;
A8: (Col ((0. (R,n)),k)) . i9 = 0. R

proof

width A = n by A4, MATRIX_0:23;
then i9 in Seg (len (0. (R,n))) by A6, MATRIX_0:24;
then A9: i9 in dom (0. (R,n)) by FINSEQ_1:def 3;
A10: ( width (0. (R,n)) = n & len (0. (R,n)) = n ) by MATRIX_0:24;
k in Seg (len (0. (R,n))) by A1, FINSEQ_1:def 3;
then [i9,k] in [:(dom (0. (R,n))),(Seg (width (0. (R,n)))):] by A9, A10, ZFMISC_1:87;
then A11: [i9,k] in Indices (0. (R,n)) by MATRIX_0:def 4;
(Col ((0. (R,n)),k)) . i9 = (0. (R,n)) * (i9,k) by A9, MATRIX_0:def 8;
hence (Col ((0. (R,n)),k)) . i9 = 0. R by A11, MATRIX_1:1; :: thesis: verum

end;

reconsider a2 = (Col ((0. (R,n)),k)) . i9, a1 = (Line (A,i)) . i9 as Element of R by A8, A7;
thus (mlt ((Line (A,i)),(Col ((0. (R,n)),k)))) . i9 = a1 * a2 by A3, FVSUM_1:60
.= 0. R by A8 ; :: thesis: verum

end;

suppose m = 0 ; :: thesis: (mlt ((Line (A,i)),(Col ((0. (R,n)),k)))) . i9 = 0. R

then width A = 0 by MATRIX_0:22;
then A12: len (Line (A,i)) = 0 ;
i9 in Seg (len (mlt ((Line (A,i)),(Col ((0. (R,n)),k))))) by A3, FINSEQ_1:def 3;
then i9 in Seg (min ((len (Line (A,i))),(len (Col ((0. (R,n)),k))))) by MATRIX_3:13;
then i9 in Seg 0 by A12, XXREAL_0:def 9;
hence (mlt ((Line (A,i)),(Col ((0. (R,n)),k)))) . i9 = 0. R ; :: thesis: verum

end;

end;

end;

thus (Line (A,i)) "*" (Col ((0. (R,n)),k)) = Sum (mlt ((Line (A,i)),(Col ((0. (R,n)),k)))) by FVSUM_1:def 9
.= 0. R by A2, MATRIX_3:35 ; :: thesis: verum