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 ;
( [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]}
;
y1 = y2
y1 = b
by A1, A2, ZFMISC_1:28;
hence
y1 = y2
by A1, A3, ZFMISC_1:28;
verum
end;
hence
{[a,b]} is Function-like
; verum