theorem Th4: :: PRVECT_2:4

for X being set
for F being Domain-Sequence
for p being FinSequence holds
( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds
p . i is Function of [:X,(F . i):],(F . i) ) ) )