let X be set ; :: thesis: ( X is constanT implies X is Function-like )
set X2 = proj2 X;
assume A1: X is constanT ; :: thesis: X is Function-like
now :: thesis: for x, y1, y2 being object st [x,y1] in X & [x,y2] in X holds
y1 = y2
let x, y1, y2 be object ; :: thesis: ( [x,y1] in X & [x,y2] in X implies y1 = y2 )
set a1 = [x,y1];
set a2 = [x,y2];
assume ( [x,y1] in X & [x,y2] in X ) ; :: thesis: y1 = y2
then ( y1 in proj2 X & y2 in proj2 X ) by XTUPLE_0:def 13;
hence y1 = y2 by A1, ZFMISC_1:def 10; :: thesis: verum
end;
hence X is Function-like by FUNCT_1:def 1; :: thesis: verum