let l, n be Nat; :: thesis: for K being Field
for a being Element of K
for A being Matrix of n,K st l in dom (1. K,n) & a <> 0. K & n > 0 holds
A * (SXCol (1. K,n),l,a) = SXCol A,l,a
let K be Field; :: thesis: for a being Element of K
for A being Matrix of n,K st l in dom (1. K,n) & a <> 0. K & n > 0 holds
A * (SXCol (1. K,n),l,a) = SXCol A,l,a
let a be Element of K; :: thesis: for A being Matrix of n,K st l in dom (1. K,n) & a <> 0. K & n > 0 holds
A * (SXCol (1. K,n),l,a) = SXCol A,l,a
let A be Matrix of n,K; :: thesis: ( l in dom (1. K,n) & a <> 0. K & n > 0 implies A * (SXCol (1. K,n),l,a) = SXCol A,l,a )
assume A1: ( l in dom (1. K,n) & a <> 0. K & n > 0 ) ; :: thesis: A * (SXCol (1. K,n),l,a) = SXCol A,l,a
A2: ( len (1. K,n) = n & width (1. K,n) = n & len A = n & width A = n ) by MATRIX_1:25;
then A3: Seg (width A) = dom (1. K,n) by FINSEQ_1:def 3;
A4: ( len (SXLine (1. K,n),l,a) = len (1. K,n) & width (SXLine (1. K,n),l,a) = width (1. K,n) ) by Def2, Th1;
A5: ( len (A @ ) = n & width (A @ ) = n ) by MATRIX_1:25;
A6: dom (1. K,n) = Seg (width (1. K,n)) by A2, FINSEQ_1:def 3;
(SXLine (A @ ),l,a) @ = ((SXLine (1. K,n),l,a) * (A @ )) @ by A1, Th7
.= ((A @ ) @ ) * ((SXLine (1. K,n),l,a) @ ) by A1, A2, A4, A5, MATRIX_3:24
.= A * ((SXLine (1. K,n),l,a) @ ) by A1, A2, MATRIX_2:15
.= A * ((SXLine ((1. K,n) @ ),l,a) @ ) by MATRIX_6:10
.= A * (SXCol (1. K,n),l,a) by A1, A6, Th16 ;
hence A * (SXCol (1. K,n),l,a) = SXCol A,l,a by A1, A3, Th16; :: thesis: verum