let D, E be non empty set ; :: thesis: for M being Matrix of D
for L being Matrix of E
for i being Nat st M = L & i in Seg (width M) holds
Col (M,i) = Col (L,i)
let M be Matrix of D; :: thesis: for L being Matrix of E
for i being Nat st M = L & i in Seg (width M) holds
Col (M,i) = Col (L,i)
let L be Matrix of E; :: thesis: for i being Nat st M = L & i in Seg (width M) holds
Col (M,i) = Col (L,i)
let i be Nat; :: thesis: ( M = L & i in Seg (width M) implies Col (M,i) = Col (L,i) )
assume AS1: ( M = L & i in Seg (width M) ) ; :: thesis: Col (M,i) = Col (L,i)
A1: ( len (Col (M,i)) = len M & ( for j being Nat st j in dom M holds
(Col (M,i)) . j = M * (j,i) ) ) by MATRIX_0:def 8;
A2: ( len (Col (L,i)) = len L & ( for j being Nat st j in dom L holds
(Col (L,i)) . j = L * (j,i) ) ) by MATRIX_0:def 8;
A3: dom (Col (M,i)) = Seg (len M) by A1, FINSEQ_1:def 3
.= dom (Col (L,i)) by AS1, A2, FINSEQ_1:def 3 ;
for j being Nat st j in dom (Col (M,i)) holds
(Col (M,i)) . j = (Col (L,i)) . j

proof

let j be Nat; :: thesis: ( j in dom (Col (M,i)) implies (Col (M,i)) . j = (Col (L,i)) . j )
assume j in dom (Col (M,i)) ; :: thesis: (Col (M,i)) . j = (Col (L,i)) . j
then j in Seg (len M) by FINSEQ_1:def 3, A1;
then A4: j in dom M by FINSEQ_1:def 3;
then [j,i] in Indices M by AS1, ZFMISC_1:87;
then A5: M * (j,i) = L * (j,i) by AS1, EQ2;
thus (Col (M,i)) . j = M * (j,i) by A4, MATRIX_0:def 8
.= (Col (L,i)) . j by AS1, A4, A5, MATRIX_0:def 8 ; :: thesis: verum

end;

hence Col (M,i) = Col (L,i) by A3; :: thesis: verum