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 = 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