set h = the Function;
take A = { the Function}; :: thesis: ( A is with_common_domain & A is functional & not A is empty )
for f, g being Function st f in A & g in A holds
dom f = dom g

proof

let f, g be Function; :: thesis: ( f in A & g in A implies dom f = dom g )
assume that
A1: f in A and
A2: g in A ; :: thesis: dom f = dom g
f = the Function by A1, TARSKI:def 1;
hence dom f = dom g by A2, TARSKI:def 1; :: thesis: verum

end;

hence A is with_common_domain ; :: thesis: ( A is functional & not A is empty )
thus A is functional ; :: thesis: not A is empty
thus not A is empty ; :: thesis: verum