defpred S₁[ Function] means for x being set st x in dom f holds
( ( for y, z being set st f . x = [y,z] holds
$1 . x = [z,y] ) & ( f . x = $1 . x or ex y, z being set st f . x = [y,z] ) );
let g1, g2 be Function; :: thesis: ( dom g1 = dom f & ( for x being set st x in dom f holds
( ( for y, z being set st f . x = [y,z] holds
g1 . x = [z,y] ) & ( f . x = g1 . x or ex y, z being set st f . x = [y,z] ) ) ) & dom g2 = dom f & ( for x being set st x in dom f holds
( ( for y, z being set st f . x = [y,z] holds
g2 . x = [z,y] ) & ( f . x = g2 . x or ex y, z being set st f . x = [y,z] ) ) ) implies g1 = g2 )
assume that
A8: dom g1 = dom f and
A9: S₁[g1] and
A10: dom g2 = dom f and
A11: S₁[g2] ; :: thesis: g1 = g2

now

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

now

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

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

then consider y, z being set such that
A13: f . x = [y,z] ;
( g1 . x = [z,y] & g2 . x = [z,y] ) by A9, A11, A12, A13;
hence g1 . x = g2 . x ; :: thesis: verum

end;

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

then ( g1 . x = f . x & g2 . x = f . x ) by A9, A11, A12;
hence g1 . x = g2 . x ; :: thesis: verum

end;

end;

end;

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

end;

hence g1 = g2 by A8, A10, FUNCT_1:9; :: thesis: verum