:: deftheorem Def6 defines underlay CATALG_1:def 6 :
for S being ManySortedSign st ( for x being object st x in proj2 ( the carrier of S \/ the carrier' of S) holds
x is Function ) holds
for b₂ being set holds
( b₂ = underlay S iff for x being object holds
( x in b₂ iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) );