let k, l, n, m be Nat; :: thesis: for K being comRing
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 comRing; :: 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 that
A1: l in Seg (width M) and
A2: k in Seg (width M) and
A3: n > 0 and
A4: m > 0 and
A5: M1 = M @ ; :: thesis: (RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a)
A6: width M = m by A3, MATRIX_0:23;
then A7: len M1 = m by A4, A5, MATRIX_0:54;
A8: width (RLineXS (M1,l,k,a)) = width M1 by Th1;
len M = n by A3, MATRIX_0:23;
then A9: width M1 = n by A4, A5, A6, MATRIX_0:54;
then A10: len ((RLineXS (M1,l,k,a)) @) = n by A3, A8, MATRIX_0:54;
A11: dom M1 = Seg (len M1) by FINSEQ_1:def 3
.= Seg (width M) by A4, A5, A6, MATRIX_0:54 ;
then len (RLineXS (M1,l,k,a)) = len M1 by A2, Def3;
then width ((RLineXS (M1,l,k,a)) @) = m by A3, A7, A9, A8, MATRIX_0:54;
then A12: (RLineXS (M1,l,k,a)) @ is Matrix of n,m,K by A3, A10, MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A13: M2 = (RLineXS (M1,l,k,a)) @ ;
A14: 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 that
A15: i in dom M and
A16: 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) ) )
A17: [i,j] in Indices M by A15, A16, ZFMISC_1:87;
then A18: [j,i] in Indices M1 by A5, MATRIX_0:def 6;
then A19: i in Seg (width M1) by ZFMISC_1:87;
A20: len M1 = width M by A5, MATRIX_0:def 6;
then A21: k in dom M1 by A2, FINSEQ_1:def 3;
dom (RLineXS (M1,l,k,a)) = Seg (len (RLineXS (M1,l,k,a))) by FINSEQ_1:def 3
.= Seg (len M1) by A2, A11, Def3
.= dom M1 by FINSEQ_1:def 3 ;
then A22: [j,i] in Indices (RLineXS (M1,l,k,a)) by A18, Th1;
A23: l in dom M1 by A1, A20, FINSEQ_1:def 3;
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

A24: [i,k] in Indices M by A2, A15, ZFMISC_1:87;
assume A25: j = l ; :: thesis: M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l))
M2 * (i,j) = (RLineXS (M1,l,k,a)) * (j,i) by A13, A22, MATRIX_0:def 6
.= (a * (M1 * (k,i))) + (M1 * (l,i)) by A23, A21, A19, A25, Def3
.= (a * (M * (i,k))) + (M1 * (l,i)) by A5, A24, MATRIX_0:def 6
.= (a * (M * (i,k))) + (M * (i,l)) by A5, A17, A25, MATRIX_0:def 6 ;
hence M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ; :: thesis: verum

end;

A26: j in dom M1 by A18, ZFMISC_1:87;
thus ( j <> l implies M2 * (i,j) = M * (i,j) ) :: thesis: verum

proof

assume A27: j <> l ; :: thesis: M2 * (i,j) = M * (i,j)
M2 * (i,j) = (RLineXS (M1,l,k,a)) * (j,i) by A13, A22, MATRIX_0:def 6
.= M1 * (j,i) by A21, A26, A19, A27, Def3
.= M * (i,j) by A5, A17, MATRIX_0:def 6 ;
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

A28: Indices M = Indices (RColXS (M,l,k,a)) by MATRIX_0:26;
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 [i,j] in Indices (RColXS (M,l,k,a)) ; :: thesis: (RColXS (M,l,k,a)) * (i,j) = ((RLineXS (M1,l,k,a)) @) * (i,j)
then A29: ( i in dom M & j in Seg (width M) ) by A28, ZFMISC_1:87;
then A30: ( j = l implies ((RLineXS (M1,l,k,a)) @) * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) by A13, A14;
A31: ( j <> l implies ((RLineXS (M1,l,k,a)) @) * (i,j) = M * (i,j) ) by A13, A14, A29;
( j = l implies (RColXS (M,l,k,a)) * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) by A2, A3, A4, A29, Def6;
hence (RColXS (M,l,k,a)) * (i,j) = ((RLineXS (M1,l,k,a)) @) * (i,j) by A1, A2, A3, A4, A29, A30, A31, Def6; :: thesis: verum

end;

hence (RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a) by A12, MATRIX_0:27; :: thesis: verum