let n, m be Nat; :: thesis: for K being non empty doubleLoopStr
for M1 being Matrix of 0 ,n,K
for M2 being Matrix of 0 ,m,K holds M1 = M2
let K be non empty doubleLoopStr ; :: thesis: for M1 being Matrix of 0 ,n,K
for M2 being Matrix of 0 ,m,K holds M1 = M2
let M1 be Matrix of 0 ,n,K; :: thesis: for M2 being Matrix of 0 ,m,K holds M1 = M2
let M2 be Matrix of 0 ,m,K; :: thesis: M1 = M2
( len M1 = 0 & len M2 = 0 ) by Def3;
hence M1 = M2 by CARD_2:83; :: thesis: verum