let D be non empty set ; 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; ( width M > 0 implies ( len (M @) = width M & width (M @) = len M ) )
assume A1:
width M > 0
; ( len (M @) = width M & width (M @) = len M )
thus
len (M @) = width M
by Def6; width (M @) = len M
per cases
( len M = 0 or len M > 0 )
;
suppose A2:
len M > 0
;
width (M @) = len MA3:
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 ;
( [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):] )
( [i,j] in [:(Seg (width M)),(dom M):] implies [i,j] in [:(dom (M @)),(Seg (width (M @))):] )
assume A5:
[i,j] in [:(Seg (width M)),(dom M):]
;
[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 @))):]
;
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;
verum end; end;