A1: for x being set st x in {{} } holds
x is Function by TARSKI:def 1;
for f, g being Function st f in {{} } & g in {{} } holds
dom f = dom g

proof

let f, g be Function; :: thesis: ( f in {{} } & g in {{} } implies dom f = dom g )
assume ( f in {{} } & g in {{} } ) ; :: thesis: dom f = dom g
then ( f = {} & g = {} ) by TARSKI:def 1;
hence dom f = dom g ; :: thesis: verum

end;

hence {{} } is functional with_common_domain set by A1, Def10, FRAENKEL:def 1; :: thesis: verum