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

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