A1: dom (doms {}) = {} " (SubFuncs {}) by Def2, RELAT_1:60;
then A2: product (doms {}) = {{}} by CARD_3:19, RELAT_1:64, RELAT_1:172;

A3: now

let x be set ; :: thesis: ( x in {{}} implies (Frege {}) . x = {} )
assume A4: x in {{}} ; :: thesis: (Frege {}) . x = {}
then A5: x = {} by TARSKI:def 1;
then ex h being Function st
( (Frege {}) . {} = h & dom h = {} " (SubFuncs (rng {})) & ( for x being set st x in dom h holds
h . x = (uncurry {}) . (x,({} . x)) ) ) by A2, A4, Def7;
hence (Frege {}) . x = {} by A5, RELAT_1:172; :: thesis: verum

end;

A6: meet {} = {} by SETFAM_1:def 1;
{} " (SubFuncs {}) = {} by RELAT_1:172;
then rng (doms {}) = {} by A1, RELAT_1:60, RELAT_1:64;
then dom <:{}:> = {} by A6, Th49;
hence <:{}:> = {} ; :: thesis: Frege {} = {} .--> {}
dom (Frege {}) = product (doms {}) by Def7;
hence Frege {} = {} .--> {} by A2, A3, FUNCOP_1:17; :: thesis: verum