let D be non empty set ; :: thesis: for M being Matrix of D st width M > 0 holds
( len (M @) = width M & width (M @) = len M )
let M be Matrix of D; :: thesis: ( width M > 0 implies ( len (M @) = width M & width (M @) = len M ) )
assume A1: width M > 0 ; :: thesis: ( len (M @) = width M & width (M @) = len M )
thus len (M @) = width M by MATRIX_1:def 6; :: thesis: width (M @) = len M

per cases ( len M = 0 or len M > 0 ) ;

suppose len M = 0 ; :: thesis: width (M @) = len M

hence width (M @) = len M by A1, MATRIX_1:def 3; :: thesis: verum

end;

suppose A2: len M > 0 ; :: thesis: width (M @) = len M

for i, j being set holds
( [i,j] in [:(dom (M @)),(Seg (width (M @))):] iff [i,j] in [:(Seg (width M)),(dom M):] )

proof

let i, j be set ; :: thesis: ( [i,j] in [:(dom (M @)),(Seg (width (M @))):] iff [i,j] in [:(Seg (width M)),(dom M):] )
thus ( [i,j] in [:(dom (M @)),(Seg (width (M @))):] implies [i,j] in [:(Seg (width M)),(dom M):] ) :: thesis: ( [i,j] in [:(Seg (width M)),(dom M):] implies [i,j] in [:(dom (M @)),(Seg (width (M @))):] )

proof

assume A3: [i,j] in [:(dom (M @)),(Seg (width (M @))):] ; :: thesis: [i,j] in [:(Seg (width M)),(dom M):]
then ( i in dom (M @) & j in Seg (width (M @)) ) by ZFMISC_1:87;
then reconsider i = i, j = j as Nat ;
[i,j] in Indices (M @) by A3;
then [j,i] in Indices M by MATRIX_1:def 6;
hence [i,j] in [:(Seg (width M)),(dom M):] by ZFMISC_1:88; :: thesis: verum

end;

assume A4: [i,j] in [:(Seg (width M)),(dom M):] ; :: thesis: [i,j] in [:(dom (M @)),(Seg (width (M @))):]
then ( i in Seg (width M) & j in dom M ) by ZFMISC_1:87;
then reconsider i = i, j = j as Nat ;
[j,i] in Indices M by A4, ZFMISC_1:88;
then [i,j] in Indices (M @) by MATRIX_1:def 6;
hence [i,j] in [:(dom (M @)),(Seg (width (M @))):] ; :: thesis: verum

end;

then ( dom M = Seg (len M) & [:(Seg (width M)),(dom M):] = [:(dom (M @)),(Seg (width (M @))):] ) by FINSEQ_1:def 3, ZFMISC_1:89;
then dom M = Seg (width (M @)) by A1, A2, ZFMISC_1:110;
hence width (M @) = len M by FINSEQ_1:def 3; :: thesis: verum

end;

end;