theorem Th58: :: MATRIXJ1:58

for K being Field
for f, g being FinSequence of NAT holds 1. (K,(f ^ g)) = (1. (K,f)) ^ (1. (K,g))