theorem Th15: :: PRVECT_1:15

for a being Domain-Sequence
for u being UnOps of a
for f being Element of product a
for i being Element of dom a holds ((Frege u) . f) . i = (u . i) . (f . i)