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 not 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 not f . x1 = [y1,z1] ) ) ; :: thesis: b₁ = b₂

per cases ( f . x2 = (f ~) . x2 or ex y2, z2 being object st f . x2 = [y2,z2] ) by A2, FUNCOP_1:def 1;

suppose f . x2 = (f ~) . x2 ; :: thesis: b₁ = b₂

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

end;

suppose ex y2, z2 being object st f . x2 = [y2,z2] ; :: thesis: b₁ = b₂

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

end;

end;

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] ;
A6: (f ~) . x1 = [z1,y1] by A2, A5, FUNCOP_1:def 1;

per cases ( ( f . x2 = (f ~) . x2 & ( for y2, z2 being object holds not f . x2 = [y2,z2] ) ) or ex y2, z2 being object st f . x2 = [y2,z2] ) by A2, FUNCOP_1:def 1;

suppose ( f . x2 = (f ~) . x2 & ( for y2, z2 being object holds not f . x2 = [y2,z2] ) ) ; :: thesis: b₁ = b₂

hence x1 = x2 by A1, A6; :: thesis: verum

end;

suppose ex y2, z2 being object st f . x2 = [y2,z2] ; :: thesis: b₁ = b₂

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

end;

end;

end;

end;

end;

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