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 Def7; :: thesis: width (M @) = len M
A2: len M >= 0 by NAT_1:2;

per cases ( len M = 0 or len M > 0 ) by A2, XXREAL_0:1;

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

hence width (M @) = len M by A1, Def4; :: thesis: verum

end;

suppose A3: 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 A4: [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:106;
then reconsider i = i, j = j as Element of NAT ;
[i,j] in Indices (M @) by A4;
then [j,i] in Indices M by Def7;
hence [i,j] in [:(Seg (width M)),(dom M):] by ZFMISC_1:107; :: thesis: verum

end;

assume A5: [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:106;
then reconsider i = i, j = j as Element of NAT ;
[j,i] in Indices M by A5, ZFMISC_1:107;
then [i,j] in Indices (M @) by Def7;
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:108;
then dom M = Seg (width (M @)) by A1, A3, ZFMISC_1:134;
hence width (M @) = len M by FINSEQ_1:def 3; :: thesis: verum

end;

end;