let n be Nat; :: thesis: for D being non empty set
for M being Matrix of n,D holds
( len M = n & width M = n & Indices M = [:(Seg n),(Seg n):] )
let D be non empty set ; :: thesis: for M being Matrix of n,D holds
( len M = n & width M = n & Indices M = [:(Seg n),(Seg n):] )
let M be Matrix of n,D; :: thesis: ( len M = n & width M = n & Indices M = [:(Seg n),(Seg n):] )
A1: len M = n by Def2;

A2: now :: thesis: ( ( n = 0 & width M = 0 ) or ( n > 0 & width M = n ) )

per cases ( n = 0 or n > 0 ) ;

case n = 0 ; :: thesis: width M = 0

hence width M = 0 by A1, Def3; :: thesis: verum

end;

case n > 0 ; :: thesis: width M = n

hence width M = n by A1, Th20; :: thesis: verum

end;

end;

end;

Seg (len M) = dom M by FINSEQ_1:def 3;
hence ( len M = n & width M = n & Indices M = [:(Seg n),(Seg n):] ) by A2, Def2; :: thesis: verum