set f = {[x,y]};
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom {[x,y]} or not x2 in dom {[x,y]} or not {[x,y]} . x1 = {[x,y]} . x2 or x1 = x2 )
assume ( x1 in dom {[x,y]} & x2 in dom {[x,y]} & {[x,y]} . x1 = {[x,y]} . x2 ) ; :: thesis: x1 = x2
then A1: ( x1 in {x} & x2 in {x} ) by RELAT_1:9;
hence x1 = x by TARSKI:def 1
.= x2 by A1, TARSKI:def 1 ;
:: thesis: verum