consider y being set such that
W: y in Y by XBOOLE_0:def 1;
reconsider y = y as Element of Y by W;
take X --> y ; :: thesis: X --> y is total
thus X --> y is total ; :: thesis: verum