theorem Th30: :: ACKERMAN:30

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