let X be set ; :: thesis: for f, g being Function st dom f = X & dom g = X holds
dom <:f,g:> = X
let f, g be Function; :: thesis: ( dom f = X & dom g = X implies dom <:f,g:> = X )
dom <:f,g:> = (dom f) /\ (dom g) by Def7;
hence ( dom f = X & dom g = X implies dom <:f,g:> = X ) ; :: thesis: verum