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

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