set X = {[a,b]};
A1: [:{a},{b}:] = {[a,b]} by ZFMISC_1:29;
for x, y1, y2 being object st [x,y1] in {[a,b]} & [x,y2] in {[a,b]} holds
y1 = y2
proof
let x, y1, y2 be object ; :: thesis: ( [x,y1] in {[a,b]} & [x,y2] in {[a,b]} implies y1 = y2 )
assume that
A2: [x,y1] in {[a,b]} and
A3: [x,y2] in {[a,b]} ; :: thesis: y1 = y2
y1 = b by A1, A2, ZFMISC_1:28;
hence y1 = y2 by A1, A3, ZFMISC_1:28; :: thesis: verum
end;
hence {[a,b]} is Function-like ; :: thesis: verum