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