let D1, D2 be non empty set ; :: thesis: for M1 being Matrix of D1
for M2 being Matrix of D2 st M1 = M2 holds
for j being Nat st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)
let M1 be Matrix of D1; :: thesis: for M2 being Matrix of D2 st M1 = M2 holds
for j being Nat st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)
let M2 be Matrix of D2; :: thesis: ( M1 = M2 implies for j being Nat st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j) )
assume A1: M1 = M2 ; :: thesis: for j being Nat st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)

hereby :: thesis: verum

let j be Nat; :: thesis: ( j in Seg (width M1) implies Col (M1,j) = Col (M2,j) )
assume A2: j in Seg (width M1) ; :: thesis: Col (M1,j) = Col (M2,j)
A3: for k being Nat st k in dom (Col (M1,j)) holds
(Col (M1,j)) . k = (Col (M2,j)) . k

proof

let k be Nat; :: thesis: ( k in dom (Col (M1,j)) implies (Col (M1,j)) . k = (Col (M2,j)) . k )
assume k in dom (Col (M1,j)) ; :: thesis: (Col (M1,j)) . k = (Col (M2,j)) . k
then k in Seg (len (Col (M1,j))) by FINSEQ_1:def 3;
then A4: k in Seg (len M1) by MATRIX_0:def 8;
then A5: [k,j] in Indices M1 by A2, Th12;
A6: k in dom M1 by A4, FINSEQ_1:def 3;
hence (Col (M1,j)) . k = M1 * (k,j) by MATRIX_0:def 8
.= M2 * (k,j) by A1, A5, MATRIXR1:23
.= (Col (M2,j)) . k by A1, A6, MATRIX_0:def 8 ;
:: thesis: verum

end;

dom (Col (M1,j)) = Seg (len (Col (M1,j))) by FINSEQ_1:def 3
.= Seg (len M1) by MATRIX_0:def 8
.= Seg (len (Col (M2,j))) by A1, MATRIX_0:def 8
.= dom (Col (M2,j)) by FINSEQ_1:def 3 ;
hence Col (M1,j) = Col (M2,j) by A3, FINSEQ_1:13; :: thesis: verum

end;