let f be empty Function; :: thesis: .: f = {} .--> {}
A1: dom (.: f) = bool (dom f) by FUNCT_3:def 1
.= {{}} by ZFMISC_1:1 ;
then A2: dom (.: f) = dom {[{},{}]} by RELAT_1:9
.= dom ({} .--> {}) by FUNCT_4:82 ;

now :: thesis: for x being object st x in dom (.: f) holds
(.: f) . x = ({} .--> {}) . x

let x be object ; :: thesis: ( x in dom (.: f) implies (.: f) . x = ({} .--> {}) . x )
assume x in dom (.: f) ; :: thesis: (.: f) . x = ({} .--> {}) . x
then A3: x = {} by A1, TARSKI:def 1;
hence (.: f) . x = {} by FUNCT_3:8
.= ({} .--> {}) . x by A3, FUNCOP_1:72 ;
:: thesis: verum

end;

hence .: f = {} .--> {} by A2, FUNCT_1:2; :: thesis: verum