theorem Th10: :: COMPUT_1:11

for X being set holds
( ( X is functional & X is compatible ) iff union X is Function )