theorem Th13: :: MATRIX14:13

for n being Element of NAT
for K being Field
for p1 being Element of n -tuples_on the carrier of K holds mlt (p1,(n |-> (0. K))) = n |-> (0. K)