thus A --> z is Function-like :: thesis: A --> z is Relation-like

proof

let x be set ; :: according to FUNCT_1:def 1 :: thesis: for b₁, b₂ being set holds
( not [x,b₁] in A --> z or not [x,b₂] in A --> z or b₁ = b₂ )
let y1, y2 be set ; :: thesis: ( not [x,y1] in A --> z or not [x,y2] in A --> z or y1 = y2 )
assume ( [x,y1] in A --> z & [x,y2] in A --> z ) ; :: thesis: y1 = y2
then ( y1 in {z} & y2 in {z} ) by ZFMISC_1:106;
then ( y1 = z & y2 = z ) by TARSKI:def 1;
hence y1 = y2 ; :: thesis: verum

end;

thus for x being set st x in A --> z holds
ex y1, y2 being set st [y1,y2] = x by RELAT_1:def 1; :: according to RELAT_1:def 1 :: thesis: verum