let f be Function; :: thesis: ( [:{} ,f:] = {} & [:f,{} :] = {} )
( dom [:{} ,f:] = [:(dom {} ),(dom f):] & dom [:f,{} :] = [:(dom f),(dom {} ):] ) by FUNCT_3:def 9;
then ( dom [:{} ,f:] = {} & dom [:f,{} :] = {} ) by ZFMISC_1:113;
hence ( [:{} ,f:] = {} & [:f,{} :] = {} ) ; :: thesis: verum