now :: thesis: for x1, x2 being object st x1 in dom (f ~) & x2 in dom (f ~) & (f ~) . x1 = (f ~) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (f ~) & x2 in dom (f ~) & (f ~) . x1 = (f ~) . x2 implies b₁ = b₂ )
assume A1: ( x1 in dom (f ~) & x2 in dom (f ~) & (f ~) . x1 = (f ~) . x2 ) ; :: thesis: b₁ = b₂
then A2: ( x1 in dom f & x2 in dom f ) by FUNCOP_1:def 1;

per cases then ( ( f . x1 = (f ~) . x1 & ( for y1, z1 being object holds f . x1 <> [y1,z1] ) ) or ex y1, z1 being object st f . x1 = [y1,z1] ) by FUNCOP_1:def 1;

suppose A3: ( f . x1 = (f ~) . x1 & ( for y1, z1 being object holds f . x1 <> [y1,z1] ) ) ; :: thesis: b₁ = b₂

f . x2 = (f ~) . x2

proof

assume f . x2 <> (f ~) . x2 ; :: thesis: contradiction
then consider y2, z2 being object such that
A4: f . x2 = [y2,z2] by A2, FUNCOP_1:def 1;
[z2,y2] = (f ~) . x1 by A1, A2, A4, FUNCOP_1:def 1;
then [y2,z2] = ((f ~) ~) . x1 by A1, FUNCOP_1:def 1
.= f . x1 ;
hence contradiction by A3; :: thesis: verum

end;

hence x1 = x2 by A1, A2, A3, FUNCT_1:def 4; :: thesis: verum

end;

suppose ex y1, z1 being object st f . x1 = [y1,z1] ; :: thesis: b₁ = b₂

then consider y1, z1 being object such that
A5: f . x1 = [y1,z1] ;
[z1,y1] = (f ~) . x2 by A1, A2, A5, FUNCOP_1:def 1;
then [y1,z1] = ((f ~) ~) . x2 by A1, FUNCOP_1:def 1
.= f . x2 ;
hence x1 = x2 by A2, A5, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence f ~ is one-to-one by FUNCT_1:def 4; :: thesis: verum