now :: thesis: for x being object st x in X \/ Y holds
x is Function
let x be object ; :: thesis: ( x in X \/ Y implies x is Function )
assume x in X \/ Y ; :: thesis: x is Function
then ( x in X or x in Y ) by XBOOLE_0:def 3;
hence x is Function ; :: thesis: verum
end;
hence X \/ Y is functional by FUNCT_1:def 13; :: thesis: verum