A1: ( dom (doms {} ) = {} " (SubFuncs {} ) & {} " (SubFuncs {} ) = {} ) by Def2, RELAT_1:60, RELAT_1:172;
then ( rng (doms {} ) = {} & meet {} = {} & meet (doms {} ) = meet (rng (doms {} )) ) by RELAT_1:60, RELAT_1:64, SETFAM_1:def 1;
then dom <:{} :> = {} by Th49;
hence <:{} :> = {} ; :: thesis: Frege {} = {} .--> {}
A2: ( dom (Frege {} ) = product (doms {} ) & product (doms {} ) = {{} } ) by A1, Def7, CARD_3:19, RELAT_1:64;

now

let x be set ; :: thesis: ( x in {{} } implies (Frege {} ) . x = {} )
assume A3: x in {{} } ; :: thesis: (Frege {} ) . x = {}
then A4: 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, A3, Def7;
hence (Frege {} ) . x = {} by A4, RELAT_1:172; :: thesis: verum

end;

hence Frege {} = {} .--> {} by A2, FUNCOP_1:17; :: thesis: verum