let l, n, k be Nat; :: thesis: for K being Field
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 Field; :: 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_1:25;
A4: width (1. K,n) = n by MATRIX_1:25;
then A5: dom (1. K,n) = Seg (width (1. K,n)) by A3, FINSEQ_1:def 3;
A6: width (A @ ) = n by MATRIX_1:25;
A7: ( width (ILine (1. K,n),l,k) = width (1. K,n) & len (A @ ) = n ) by Th1, MATRIX_1:25;
A8: len A = n by MATRIX_1:25;
A9: width A = n by MATRIX_1:25;
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:24
.= A * ((ILine (1. K,n),l,k) @ ) by A2, A8, A9, MATRIX_2:15
.= 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