theorem Th34: :: MATRPROB:34

for i being Nat
for e1, e2 being Element of i -tuples_on REAL
for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)