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 object ; :: according to FUNCT_1:def 1 :: thesis: ( not [y,y1] in [:A,{x}:] or not [y,y2] in [:A,{x}:] or y1 = y2 )
assume that
A1: [y,y1] in [:A,{x}:] and
A2: [y,y2] in [:A,{x}:] ; :: thesis: y1 = y2
y1 = x by A1, ZFMISC_1:106;
hence y1 = y2 by A2, ZFMISC_1:106; :: thesis: verum
end;
hence [:A,{x}:] is Function ; :: thesis: verum