let K be Ring; :: thesis: for n, m being Nat holds
( len (0. (K,n,m)) = n & dom (0. (K,n,m)) = Seg n )
let n, m be Nat; :: thesis: ( len (0. (K,n,m)) = n & dom (0. (K,n,m)) = Seg n )
len (n |-> (m |-> (0. K))) = n by CARD_1:def 7;
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