let K be set ; :: thesis: for A, B being Matrix of K st len A = len B & width A = width B holds
Indices A = Indices B
let A, B be Matrix of K; :: thesis: ( len A = len B & width A = width B implies Indices A = Indices B )
A1: dom A = Seg (len A) by FINSEQ_1:def 3;
assume ( len A = len B & width A = width B ) ; :: thesis: Indices A = Indices B
hence Indices A = Indices B by A1, FINSEQ_1:def 3; :: thesis: verum