defpred S₁[ 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; :: thesis: ( 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: S₁[g1] and
A12: dom g2 = dom f and
A13: S₁[g2] ; :: thesis: g1 = g2

now :: thesis: for x being object st x in dom f holds
g1 . x = g2 . x

let x be object ; :: thesis: ( x in dom f implies g1 . x = g2 . x )
assume A14: x in dom f ; :: thesis: g1 . x = g2 . x

now :: thesis: g1 . x = g2 . x

per cases ( ex y, z being object st f . x = [y,z] or for y, z being object holds not f . x = [y,z] ) ;

suppose ex y, z being object st f . x = [y,z] ; :: thesis: g1 . x = g2 . x

then consider y, z being object such that
A15: f . x = [y,z] ;
g1 . x = [z,y] by A11, A14, A15;
hence g1 . x = g2 . x by A13, A14, A15; :: thesis: verum

end;

suppose A16: for y, z being object holds not f . x = [y,z] ; :: thesis: g1 . x = g2 . x

then g1 . x = f . x by A11, A14;
hence g1 . x = g2 . x by A13, A14, A16; :: thesis: verum

end;

end;

end;

hence g1 . x = g2 . x ; :: thesis: verum

end;

hence g1 = g2 by A10, A12; :: thesis: verum