let k, l, n be Nat; :: thesis: for K being comRing
for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds
A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k)
let K be comRing; :: thesis: for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds
A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k)
let A be Matrix of n,K; :: thesis: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 implies A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k) )
assume that
A1: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) ) and
A2: n > 0 ; :: thesis: A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k)
A3: len (1. (K,n)) = n by MATRIX_0:24;
A4: width (1. (K,n)) = n by MATRIX_0:24;
then A5: dom (1. (K,n)) = Seg (width (1. (K,n))) by A3, FINSEQ_1:def 3;
A6: width (A @) = n by MATRIX_0:24;
A7: ( width (ILine ((1. (K,n)),l,k)) = width (1. (K,n)) & len (A @) = n ) by Th1, MATRIX_0:24;
A8: len A = n by MATRIX_0:24;
A9: width A = n by MATRIX_0:24;
then A10: Seg (width A) = dom (1. (K,n)) by A3, FINSEQ_1:def 3;
(ILine ((A @),l,k)) @ = ((ILine ((1. (K,n)),l,k)) * (A @)) @ by A1, Th6
.= ((A @) @) * ((ILine ((1. (K,n)),l,k)) @) by A2, A4, A7, A6, MATRIX_3:22
.= A * ((ILine ((1. (K,n)),l,k)) @) by A2, A8, A9, MATRIX_0:57
.= A * ((ILine (((1. (K,n)) @),l,k)) @) by MATRIX_6:10
.= A * (ICol ((1. (K,n)),l,k)) by A1, A2, A5, Th15 ;
hence A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k) by A1, A2, A10, Th15; :: thesis: verum