let n, m be Nat; :: thesis: for D being non empty set
for M1 being Matrix of 0 ,n,D
for M2 being Matrix of 0 ,m,D holds M1 = M2
let D be non empty set ; :: thesis: for M1 being Matrix of 0 ,n,D
for M2 being Matrix of 0 ,m,D holds M1 = M2
let M1 be Matrix of 0 ,n,D; :: thesis: for M2 being Matrix of 0 ,m,D holds M1 = M2
let M2 be Matrix of 0 ,m,D; :: thesis: M1 = M2
( len M1 = 0 & len M2 = 0 ) by Def2;
hence M1 = M2 by CARD_2:64; :: thesis: verum