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

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