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 that
A1: f in {{}} and
A2: g in {{}} ; :: thesis: dom f = dom g
f = {} by A1, TARSKI:def 1;
hence dom f = dom g by A2, TARSKI:def 1; :: thesis: verum

end;

hence {{}} is functional with_common_domain set by Def10; :: thesis: verum