A1: dom (doms {}) = {} " {} by Def1, RELAT_1:38;
then A2: product (doms {}) = {{}} by CARD_3:10, RELAT_1:41;

A3: now :: thesis: for x being object st x in {{}} holds
(Frege {}) . x = {}

let x be object ; :: 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 = dom {} & ( for x being object st x in dom h holds
h . x = (uncurry {}) . (x,({} . x)) ) ) by A2, A4, Def6;
hence (Frege {}) . x = {} by A5; :: thesis: verum

end;

A6: meet {} = {} by SETFAM_1:def 1;
rng (doms {}) = {} by A1, RELAT_1:38, RELAT_1:41;
then dom <:{}:> = {} by A6, Th25;
hence <:{}:> = {} ; :: thesis: Frege {} = {} .--> {}
dom (Frege {}) = product (doms {}) by Def6;
hence Frege {} = {} .--> {} by A2, A3, FUNCOP_1:11; :: thesis: verum