let K be Field; :: thesis: for n, m being Element of NAT holds
( len (0. K,n,m) = n & dom (0. K,n,m) = Seg n )
let n, m be Element of NAT ; :: thesis: ( len (0. K,n,m) = n & dom (0. K,n,m) = Seg n )
len (n |-> (m |-> (0. K))) = n by FINSEQ_1:def 18;
hence len (0. K,n,m) = n by MATRIX_3:def 1; :: thesis: dom (0. K,n,m) = Seg n
hence dom (0. K,n,m) = Seg n by FINSEQ_1:def 3; :: thesis: verum