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;