let l, 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) & n > 0 & m > 0 & M1 = M @ holds
(SXLine M1,l,a) @ = SXCol M,l,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) & 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_1:24;
A6: width (SXLine M1,l,a) = width M1 by Th1;
len M = n by A2, MATRIX_1:24;
then A7: width M1 = n by A3, A4, A5, MATRIX_2:12;
then A8: len ((SXLine M1,l,a) @ ) = n by A2, A6, MATRIX_2:12;
A9: len (SXLine M1,l,a) = len M1 by Def2;
len M1 = m by A3, A4, A5, MATRIX_2:12;
then width ((SXLine M1,l,a) @ ) = m by A2, A7, A9, A6, MATRIX_2:12;
then A10: (SXLine M1,l,a) @ is Matrix of n,m,K by A2, A8, MATRIX_1: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:106;
then A14: [j,i] in Indices M1 by A4, MATRIX_1:def 7;
then A15: ( j in dom M1 & i in Seg (width M1) ) by ZFMISC_1:106;
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_1:def 7
.= a * (M1 * l,i) by A15, A17, Def2
.= a * (M * i,l) by A4, A13, A17, MATRIX_1:def 7 ;
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_1:def 7
.= M1 * j,i by A15, A18, Def2
.= M * i,j by A4, A13, MATRIX_1:def 7 ;
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_1:27;
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:106;
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_1:28; :: thesis: verum