theorem Th20: :: PRVECT_1:20

for a being Domain-Sequence
for b being BinOps of a
for u being UnOps of a st ( for i being Element of dom a holds
( u . i is_an_inverseOp_wrt b . i & b . i is having_a_unity ) ) holds
Frege u is_an_inverseOp_wrt [:b:]