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