let f be Function; :: thesis: ( <:{},f:> = {} & <:f,{}:> = {} )
( dom <:{},f:> = (dom {}) /\ (dom f) & dom <:f,{}:> = (dom f) /\ (dom {}) ) by FUNCT_3:def 7;
hence ( <:{},f:> = {} & <:f,{}:> = {} ) ; :: thesis: verum