let g be Subset of f; :: thesis: g is Function-like
let x be set ; :: according to FUNCT_1:def 1 :: thesis: for y1, y2 being set st [x,y1] in g & [x,y2] in g holds
y1 = y2
let y1, y2 be set ; :: thesis: ( [x,y1] in g & [x,y2] in g implies y1 = y2 )
assume ( [x,y1] in g & [x,y2] in g ) ; :: thesis: y1 = y2
hence y1 = y2 by Def1; :: thesis: verum