let 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) & n > 0 & m > 0 & M1 = M @ holds
(SXLine (M1,l,a)) @ = SXCol (M,l,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) & n > 0 & m > 0 & M1 = M @ holds
(SXLine (M1,l,a)) @ = SXCol (M,l,a)
let a be Element of K; :: thesis: for M, M1 being Matrix of n,m,K st l in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds
(SXLine (M1,l,a)) @ = SXCol (M,l,a)
let M, M1 be Matrix of n,m,K; :: thesis: ( l in Seg (width M) & n > 0 & m > 0 & M1 = M @ implies (SXLine (M1,l,a)) @ = SXCol (M,l,a) )
assume that
A1: l in Seg (width M) and
A2: n > 0 and
A3: m > 0 and
A4: M1 = M @ ; :: thesis: (SXLine (M1,l,a)) @ = SXCol (M,l,a)
A5: width M = m by A2, MATRIX_0:23;
A6: width (SXLine (M1,l,a)) = width M1 by Th1;
len M = n by A2, MATRIX_0:23;
then A7: width M1 = n by A3, A4, A5, MATRIX_0:54;
then A8: len ((SXLine (M1,l,a)) @) = n by A2, A6, MATRIX_0:54;
A9: len (SXLine (M1,l,a)) = len M1 by Def2;
len M1 = m by A3, A4, A5, MATRIX_0:54;
then width ((SXLine (M1,l,a)) @) = m by A2, A7, A9, A6, MATRIX_0:54;
then A10: (SXLine (M1,l,a)) @ is Matrix of n,m,K by A2, A8, MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A11: M2 = (SXLine (M1,l,a)) @ ;
A12: 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,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,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) )
assume ( i in dom M & j in Seg (width M) ) ; :: thesis: ( ( j = l implies M2 * (i,j) = a * (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) )
then A13: [i,j] in Indices M by ZFMISC_1:87;
then A14: [j,i] in Indices M1 by A4, MATRIX_0:def 6;
then A15: ( j in dom M1 & i in Seg (width M1) ) by ZFMISC_1:87;
dom (SXLine (M1,l,a)) = Seg (len (SXLine (M1,l,a))) by FINSEQ_1:def 3
.= Seg (len M1) by Def2
.= dom M1 by FINSEQ_1:def 3 ;
then A16: [j,i] in Indices (SXLine (M1,l,a)) by A14, Th1;
thus ( j = l implies M2 * (i,j) = a * (M * (i,l)) ) :: thesis: ( j <> l implies M2 * (i,j) = M * (i,j) )

proof

assume A17: j = l ; :: thesis: M2 * (i,j) = a * (M * (i,l))
M2 * (i,j) = (SXLine (M1,l,a)) * (j,i) by A11, A16, MATRIX_0:def 6
.= a * (M1 * (l,i)) by A15, A17, Def2
.= a * (M * (i,l)) by A4, A13, A17, MATRIX_0:def 6 ;
hence M2 * (i,j) = a * (M * (i,l)) ; :: thesis: verum

end;

assume A18: j <> l ; :: thesis: M2 * (i,j) = M * (i,j)
M2 * (i,j) = (SXLine (M1,l,a)) * (j,i) by A11, A16, MATRIX_0:def 6
.= M1 * (j,i) by A15, A18, Def2
.= M * (i,j) by A4, A13, MATRIX_0:def 6 ;
hence M2 * (i,j) = M * (i,j) ; :: thesis: verum

end;

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

proof

A19: Indices M = Indices (SXCol (M,l,a)) by MATRIX_0:26;
let i, j be Nat; :: thesis: ( [i,j] in Indices (SXCol (M,l,a)) implies (SXCol (M,l,a)) * (i,j) = ((SXLine (M1,l,a)) @) * (i,j) )
assume [i,j] in Indices (SXCol (M,l,a)) ; :: thesis: (SXCol (M,l,a)) * (i,j) = ((SXLine (M1,l,a)) @) * (i,j)
then A20: ( i in dom M & j in Seg (width M) ) by A19, ZFMISC_1:87;
then A21: ( j = l implies ((SXLine (M1,l,a)) @) * (i,j) = a * (M * (i,l)) ) by A11, A12;
A22: ( j <> l implies ((SXLine (M1,l,a)) @) * (i,j) = M * (i,j) ) by A11, A12, A20;
( j = l implies (SXCol (M,l,a)) * (i,j) = a * (M * (i,l)) ) by A2, A3, A20, Def5;
hence (SXCol (M,l,a)) * (i,j) = ((SXLine (M1,l,a)) @) * (i,j) by A1, A2, A3, A20, A21, A22, Def5; :: thesis: verum

end;

hence (SXLine (M1,l,a)) @ = SXCol (M,l,a) by A10, MATRIX_0:27; :: thesis: verum