let A, B be non empty set ; :: thesis: Inv (A,B) is one-to-one

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 (Inv (A,B)) or not y in proj1 (Inv (A,B)) or not (Inv (A,B)) . x = (Inv (A,B)) . y or x = y )

assume that

A1: ( x in dom (Inv (A,B)) & y in dom (Inv (A,B)) ) and

A2: (Inv (A,B)) . x = (Inv (A,B)) . y ; :: thesis: x = y

reconsider x1 = x, y1 = y as Element of [:A,B:] by A1, FUNCT_2:def 1;

( (Inv (A,B)) . x1 = [(x1 `2),(x1 `1)] & (Inv (A,B)) . y1 = [(y1 `2),(y1 `1)] ) by Def6;

then ( x1 `1 = y1 `1 & x1 `2 = y1 `2 ) by A2, XTUPLE_0:1;

hence x = y by DOMAIN_1:2; :: thesis: verum

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 (Inv (A,B)) or not y in proj1 (Inv (A,B)) or not (Inv (A,B)) . x = (Inv (A,B)) . y or x = y )

assume that

A1: ( x in dom (Inv (A,B)) & y in dom (Inv (A,B)) ) and

A2: (Inv (A,B)) . x = (Inv (A,B)) . y ; :: thesis: x = y

reconsider x1 = x, y1 = y as Element of [:A,B:] by A1, FUNCT_2:def 1;

( (Inv (A,B)) . x1 = [(x1 `2),(x1 `1)] & (Inv (A,B)) . y1 = [(y1 `2),(y1 `1)] ) by Def6;

then ( x1 `1 = y1 `1 & x1 `2 = y1 `2 ) by A2, XTUPLE_0:1;

hence x = y by DOMAIN_1:2; :: thesis: verum