defpred S1[ Function] means for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
$1 . x = [z,y] ) & ( f . x = $1 . x or ex y, z being object st f . x = [y,z] ) );
let g1, g2 be Function; ( dom g1 = dom f & ( for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
g1 . x = [z,y] ) & ( f . x = g1 . x or ex y, z being object st f . x = [y,z] ) ) ) & dom g2 = dom f & ( for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
g2 . x = [z,y] ) & ( f . x = g2 . x or ex y, z being object st f . x = [y,z] ) ) ) implies g1 = g2 )
assume that
A10:
dom g1 = dom f
and
A11:
S1[g1]
and
A12:
dom g2 = dom f
and
A13:
S1[g2]
; g1 = g2
hence
g1 = g2
by A10, A12; verum