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