let n, m be Nat; :: thesis: for K being Field holds - (0. (K,n,m)) = 0. (K,n,m)

let K be Field; :: thesis: - (0. (K,n,m)) = 0. (K,n,m)

let K be Field; :: thesis: - (0. (K,n,m)) = 0. (K,n,m)

per cases
( n > 0 or n = 0 )
by NAT_1:3;

end;