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,{}:] = {} ) by ZFMISC_1:90; :: thesis: verum