theorem Th70: :: MATGRP_0:58

for n being Nat
for L being non empty 1-sorted holds n -tuples_on (n -tuples_on the carrier of L) is n,L -matrix-membered