defpred S_{1}[ 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_{1}[g1]
and

A12: dom g2 = dom f and

A13: S_{1}[g2]
; :: thesis: g1 = g2

( ( 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

A12: dom g2 = dom f and

A13: S

now :: thesis: for x being object st x in dom f holds

g1 . x = g2 . x

hence
g1 = g2
by A10, A12; :: thesis: verumg1 . 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

end;assume A14: x in dom f ; :: thesis: g1 . x = g2 . x

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

hence
g1 . x = g2 . x
; :: thesis: verumper cases
( ex y, z being object st f . x = [y,z] or for y, z being object holds not f . x = [y,z] )
;

end;