let I be set ; :: thesis: for a being object holds pr1 (I,{a}) is one-to-one
let a be object ; :: thesis: pr1 (I,{a}) is one-to-one
set f = pr1 (I,{a});
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (pr1 (I,{a})) or not y in dom (pr1 (I,{a})) or not (pr1 (I,{a})) . x = (pr1 (I,{a})) . y or x = y )
assume A1: ( x in dom (pr1 (I,{a})) & y in dom (pr1 (I,{a})) ) ; :: thesis: ( not (pr1 (I,{a})) . x = (pr1 (I,{a})) . y or x = y )
then consider i1, a1 being object such that
A2: ( i1 in I & a1 in {a} & x = [i1,a1] ) by ZFMISC_1:def 2;
consider i2, a2 being object such that
A3: ( i2 in I & a2 in {a} & y = [i2,a2] ) by A1, ZFMISC_1:def 2;
assume (pr1 (I,{a})) . x = (pr1 (I,{a})) . y ; :: thesis: x = y
then (pr1 (I,{a})) . (i1,a1) = (pr1 (I,{a})) . (i2,a2) by A2, A3;
then A4: ( i1 = (pr1 (I,{a})) . (i2,a2) & (pr1 (I,{a})) . (i2,a2) = i2 ) by A2, A3, FUNCT_3:def 4;
( a1 = a & a = a2 ) by A2, A3, TARSKI:def 1;
hence x = y by A2, A3, A4; :: thesis: verum