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