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 Def6; :: 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, Def3; :: thesis: verum
end;
suppose A2: len M > 0 ; :: thesis: width (M @) = len M
A3: width (M @) in NAT by ORDINAL1:def 12;
for i, j being object holds
( [i,j] in [:(dom (M @)),(Seg (width (M @))):] iff [i,j] in [:(Seg (width M)),(dom M):] )
proof
let i, j be object ; :: 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:87;
then reconsider i = i, j = j as Nat ;
[i,j] in Indices (M @) by A4;
then [j,i] in Indices M by Def6;
hence [i,j] in [:(Seg (width M)),(dom M):] by ZFMISC_1:88; :: 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:87;
then reconsider i = i, j = j as Nat ;
[j,i] in Indices M by A5, ZFMISC_1:88;
then [i,j] in Indices (M @) by Def6;
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, A3; :: thesis: verum
end;
end;