let X be TopStruct ; :: thesis: for Y, Z being non empty TopStruct
for f being Function of X,Y
for g being Function of X,Z holds
( dom f = dom g & dom f = the carrier of X & dom f = [#] X )
let Y, Z be non empty TopStruct ; :: thesis: for f being Function of X,Y
for g being Function of X,Z holds
( dom f = dom g & dom f = the carrier of X & dom f = [#] X )
let f be Function of X,Y; :: thesis: for g being Function of X,Z holds
( dom f = dom g & dom f = the carrier of X & dom f = [#] X )
let g be Function of X,Z; :: thesis: ( dom f = dom g & dom f = the carrier of X & dom f = [#] X )
dom f = the carrier of X by FUNCT_2:def 1;
hence ( dom f = dom g & dom f = the carrier of X & dom f = [#] X ) by FUNCT_2:def 1; :: thesis: verum