let x be set ; :: according to FUNCT_1:def 1 :: thesis: for b₁, b₂ being set holds
( not [x,b₁] in f \ A or not [x,b₂] in f \ A or b₁ = b₂ )
let y1, y2 be set ; :: thesis: ( not [x,y1] in f \ A or not [x,y2] in f \ A or y1 = y2 )
assume ( [x,y1] in f \ A & [x,y2] in f \ A ) ; :: thesis: y1 = y2
then ( [x,y1] in f & [x,y2] in f ) by XBOOLE_0:def 5;
hence y1 = y2 by FUNCT_1:def 1; :: thesis: verum