let A, x be set ; :: thesis: [:A,{x}:] is Function
set X = [:A,{x}:];
[:A,{x}:] is Function-like

proof

let y, y1, y2 be set ; :: according to FUNCT_1:def 1 :: thesis: ( not [y,y1] in [:A,{x}:] or not [y,y2] in [:A,{x}:] or y1 = y2 )
assume ( [y,y1] in [:A,{x}:] & [y,y2] in [:A,{x}:] ) ; :: thesis: y1 = y2
then ( y1 = x & y2 = x ) by ZFMISC_1:129;
hence y1 = y2 ; :: thesis: verum

end;

hence [:A,{x}:] is Function ; :: thesis: verum