set x = the Element of X;
set y = the Element of Y;
take F = the Element of X .--> the Element of Y; :: thesis: ( F is X -defined & F is Y -valued & not F is empty & F is finite )
thus F is X -defined ; :: thesis: ( F is Y -valued & not F is empty & F is finite )
thus F is Y -valued ; :: thesis: ( not F is empty & F is finite )
thus ( not F is empty & F is finite ) ; :: thesis: verum