let l, k, n, m be Nat; :: thesis: for K being Field
for a being Element of K
for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds
(RLineXS M1,l,k,a) @ = RColXS M,l,k,a
let K be Field; :: thesis: for a being Element of K
for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds
(RLineXS M1,l,k,a) @ = RColXS M,l,k,a
let a be Element of K; :: thesis: for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds
(RLineXS M1,l,k,a) @ = RColXS M,l,k,a
let M, M1 be Matrix of n,m,K; :: thesis: ( l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ implies (RLineXS M1,l,k,a) @ = RColXS M,l,k,a )
assume A1: ( l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ ) ; :: thesis: (RLineXS M1,l,k,a) @ = RColXS M,l,k,a
then A2: ( len M = n & width M = m ) by MATRIX_1:24;
then A3: ( len M1 = m & width M1 = n ) by A1, MATRIX_2:12;
A4: dom M1 = Seg (len M1) by FINSEQ_1:def 3
.= Seg (width M) by A1, A2, MATRIX_2:12 ;
then ( len (RLineXS M1,l,k,a) = len M1 & width (RLineXS M1,l,k,a) = width M1 ) by A1, Def3, Th1;
then ( len ((RLineXS M1,l,k,a) @ ) = n & width ((RLineXS M1,l,k,a) @ ) = m ) by A1, A3, MATRIX_2:12;
then A5: (RLineXS M1,l,k,a) @ is Matrix of n,m,K by A1, MATRIX_1:20;
then consider M2 being Matrix of n,m,K such that
A6: M2 = (RLineXS M1,l,k,a) @ ;
A7: for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * i,j = (a * (M * i,k)) + (M * i,l) ) & ( j <> l implies M2 * i,j = M * i,j ) )

proof

let i, j be Nat; :: thesis: ( i in dom M & j in Seg (width M) implies ( ( j = l implies M2 * i,j = (a * (M * i,k)) + (M * i,l) ) & ( j <> l implies M2 * i,j = M * i,j ) ) )
assume A8: ( i in dom M & j in Seg (width M) ) ; :: thesis: ( ( j = l implies M2 * i,j = (a * (M * i,k)) + (M * i,l) ) & ( j <> l implies M2 * i,j = M * i,j ) )
len M1 = width M by A1, MATRIX_1:def 7;
then A9: ( l in dom M1 & k in dom M1 ) by A1, FINSEQ_1:def 3;
A10: [i,j] in Indices M by A8, ZFMISC_1:106;
then A11: [j,i] in Indices M1 by A1, MATRIX_1:def 7;
then A12: ( j in dom M1 & i in Seg (width M1) ) by ZFMISC_1:106;
dom (RLineXS M1,l,k,a) = Seg (len (RLineXS M1,l,k,a)) by FINSEQ_1:def 3
.= Seg (len M1) by A1, A4, Def3
.= dom M1 by FINSEQ_1:def 3 ;
then A13: [j,i] in Indices (RLineXS M1,l,k,a) by A11, Th1;
thus ( j = l implies M2 * i,j = (a * (M * i,k)) + (M * i,l) ) :: thesis: ( j <> l implies M2 * i,j = M * i,j )

proof

assume A14: j = l ; :: thesis: M2 * i,j = (a * (M * i,k)) + (M * i,l)
A15: [i,k] in Indices M by A1, A8, ZFMISC_1:106;
M2 * i,j = (RLineXS M1,l,k,a) * j,i by A6, A13, MATRIX_1:def 7
.= (a * (M1 * k,i)) + (M1 * l,i) by A9, A12, A14, Def3
.= (a * (M * i,k)) + (M1 * l,i) by A1, A15, MATRIX_1:def 7
.= (a * (M * i,k)) + (M * i,l) by A1, A10, A14, MATRIX_1:def 7 ;
hence M2 * i,j = (a * (M * i,k)) + (M * i,l) ; :: thesis: verum

end;

thus ( j <> l implies M2 * i,j = M * i,j ) :: thesis: verum

proof

assume A16: j <> l ; :: thesis: M2 * i,j = M * i,j
M2 * i,j = (RLineXS M1,l,k,a) * j,i by A6, A13, MATRIX_1:def 7
.= M1 * j,i by A9, A12, A16, Def3
.= M * i,j by A1, A10, MATRIX_1:def 7 ;
hence M2 * i,j = M * i,j ; :: thesis: verum

end;

end;

for i, j being Nat st [i,j] in Indices (RColXS M,l,k,a) holds
(RColXS M,l,k,a) * i,j = ((RLineXS M1,l,k,a) @ ) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (RColXS M,l,k,a) implies (RColXS M,l,k,a) * i,j = ((RLineXS M1,l,k,a) @ ) * i,j )
assume A17: [i,j] in Indices (RColXS M,l,k,a) ; :: thesis: (RColXS M,l,k,a) * i,j = ((RLineXS M1,l,k,a) @ ) * i,j
( Indices (RColXS M,l,k,a) = Indices ((RLineXS M1,l,k,a) @ ) & Indices M = Indices (RColXS M,l,k,a) ) by A6, MATRIX_1:27;
then ( i in dom M & j in Seg (width M) ) by A17, ZFMISC_1:106;
then ( ( j = l implies ((RLineXS M1,l,k,a) @ ) * i,j = (a * (M * i,k)) + (M * i,l) ) & ( j <> l implies ((RLineXS M1,l,k,a) @ ) * i,j = M * i,j ) & ( j = l implies (RColXS M,l,k,a) * i,j = (a * (M * i,k)) + (M * i,l) ) & ( j <> l implies (RColXS M,l,k,a) * i,j = M * i,j ) ) by A1, A6, A7, Def6;
hence (RColXS M,l,k,a) * i,j = ((RLineXS M1,l,k,a) @ ) * i,j ; :: thesis: verum

end;

hence (RLineXS M1,l,k,a) @ = RColXS M,l,k,a by A5, MATRIX_1:28; :: thesis: verum