let A, B be non empty set ; :: thesis: Inv A,B is one-to-one
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 (Inv A,B) or not b₁ in proj1 (Inv A,B) or not (Inv A,B) . x = (Inv A,B) . b₁ or x = b₁ )
let y be set ; :: 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, ZFMISC_1:33;
hence x = y by DOMAIN_1:12; :: thesis: verum