let B, X be set ; :: thesis: for D being non empty set
for f being Function of X,D holds (.: f) " B c= bool X
let D be non empty set ; :: thesis: for f being Function of X,D holds (.: f) " B c= bool X
let f be Function of X,D; :: thesis: (.: f) " B c= bool X
dom f = X by FUNCT_2:def 1;
hence (.: f) " B c= bool X by Th11; :: thesis: verum