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

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