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

ex y1, y2 being object st [y1,y2] = x by RELAT_1:def 1; :: according to RELAT_1:def 1 :: thesis: verum

proof

thus
for x being object st x in A --> z holds
let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in A --> z or not [x,y2] in A --> z or y1 = y2 )

assume that

A1: [x,y1] in A --> z and

A2: [x,y2] in A --> z ; :: thesis: y1 = y2

y1 in {z} by A1, ZFMISC_1:87;

then A3: y1 = z by TARSKI:def 1;

y2 in {z} by A2, ZFMISC_1:87;

hence y1 = y2 by A3, TARSKI:def 1; :: thesis: verum

end;assume that

A1: [x,y1] in A --> z and

A2: [x,y2] in A --> z ; :: thesis: y1 = y2

y1 in {z} by A1, ZFMISC_1:87;

then A3: y1 = z by TARSKI:def 1;

y2 in {z} by A2, ZFMISC_1:87;

hence y1 = y2 by A3, TARSKI:def 1; :: thesis: verum

ex y1, y2 being object st [y1,y2] = x by RELAT_1:def 1; :: according to RELAT_1:def 1 :: thesis: verum