theorem Th31: :: ACKERMAN:31

for D being set
for f being BinOp of D holds dom2tuple f is PartFunc of (D *),D