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