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 Element of 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 Element of 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 Element of NAT st j in Seg (width M1) holds
Col M1,j = Col M2,j )
assume A1: M1 = M2 ; :: thesis: for j being Element of NAT st j in Seg (width M1) holds
Col M1,j = Col M2,j

hereby :: thesis: verum

let j be Element of 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: dom (Col M1,j) = Seg (len (Col M1,j)) by FINSEQ_1:def 3
.= Seg (len M1) by MATRIX_1:def 9
.= Seg (len (Col M2,j)) by A1, MATRIX_1:def 9
.= dom (Col M2,j) by FINSEQ_1:def 3 ;
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 A4: k in dom (Col M1,j) ; :: thesis: (Col M1,j) . k = (Col M2,j) . k
k in Seg (len (Col M1,j)) by A4, FINSEQ_1:def 3;
then k in Seg (len M1) by MATRIX_1:def 9;
then A5: ( [k,j] in Indices M1 & k in dom M1 ) by A2, Th12, FINSEQ_1:def 3;
hence (Col M1,j) . k = M1 * k,j by MATRIX_1:def 9
.= M2 * k,j by A1, A5, MATRIXR1:23
.= (Col M2,j) . k by A1, A5, MATRIX_1:def 9 ;
:: thesis: verum

end;

hence Col M1,j = Col M2,j by A3, FINSEQ_1:17; :: thesis: verum

end;