defpred S_{1}[ object , object ] means ( ( for y, z being object st f . $1 = [y,z] holds

$2 = [z,y] ) & ( f . $1 = $2 or ex y, z being object st f . $1 = [y,z] ) );

( dom g = dom f & ( for x being object st x in dom f holds

S_{1}[x,g . x] ) )
from FUNCT_1:sch 2(A6, A1); :: thesis: verum

$2 = [z,y] ) & ( f . $1 = $2 or ex y, z being object st f . $1 = [y,z] ) );

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

ex y being object st S_{1}[x,y]

ex y being object st S

let x be object ; :: thesis: ( x in dom f implies ex y being object st S_{1}[x,y] )

assume x in dom f ; :: thesis: ex y being object st S_{1}[x,y]

_{1}[x,y]
; :: thesis: verum

end;assume x in dom f ; :: thesis: ex y being object st S

now :: thesis: ( ( ex y, z being object st f . x = [y,z] & ex y1 being object st

( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) ) ) or ( ( for y, z being object holds not f . x = [y,z] ) & ex y1 being set st

( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) ) ) )end;

hence
ex y being object st S( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) ) ) or ( ( for y, z being object holds not f . x = [y,z] ) & ex y1 being set st

( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) ) ) )

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

end;

case A2:
ex y, z being object st f . x = [y,z]
; :: thesis: ex y1 being object st

( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) )

( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) )

then consider y, z being object such that

A3: f . x = [y,z] ;

take y1 = [z,y]; :: thesis: ( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) )

thus for y, z being object st f . x = [y,z] holds

y1 = [z,y] :: thesis: ( f . x = y1 or ex y, z being object st f . x = [y,z] )

end;A3: f . x = [y,z] ;

take y1 = [z,y]; :: thesis: ( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) )

thus for y, z being object st f . x = [y,z] holds

y1 = [z,y] :: thesis: ( f . x = y1 or ex y, z being object st f . x = [y,z] )

proof

thus
( f . x = y1 or ex y, z being object st f . x = [y,z] )
by A2; :: thesis: verum
let y9, z9 be object ; :: thesis: ( f . x = [y9,z9] implies y1 = [z9,y9] )

assume A4: f . x = [y9,z9] ; :: thesis: y1 = [z9,y9]

then z = z9 by A3, XTUPLE_0:1;

hence y1 = [z9,y9] by A3, A4, XTUPLE_0:1; :: thesis: verum

end;assume A4: f . x = [y9,z9] ; :: thesis: y1 = [z9,y9]

then z = z9 by A3, XTUPLE_0:1;

hence y1 = [z9,y9] by A3, A4, XTUPLE_0:1; :: thesis: verum

case A5:
for y, z being object holds not f . x = [y,z]
; :: thesis: ex y1 being set st

( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) )

( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) )

reconsider y1 = f . x as set ;

take y1 = y1; :: thesis: ( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) )

thus ( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) ) by A5; :: thesis: verum

end;take y1 = y1; :: thesis: ( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) )

thus ( ( for y, z being object st f . x = [y,z] holds

y1 = [z,y] ) & ( f . x = y1 or ex y, z being object st f . x = [y,z] ) ) by A5; :: thesis: verum

A6: now :: thesis: for x, y1, y2 being object st x in dom f & S_{1}[x,y1] & S_{1}[x,y2] holds

y1 = y2

thus
ex g being Function st y1 = y2

let x, y1, y2 be object ; :: thesis: ( x in dom f & S_{1}[x,y1] & S_{1}[x,y2] implies y1 = y2 )

assume x in dom f ; :: thesis: ( S_{1}[x,y1] & S_{1}[x,y2] implies y1 = y2 )

assume that

A7: S_{1}[x,y1]
and

A8: S_{1}[x,y2]
; :: thesis: y1 = y2

end;assume x in dom f ; :: thesis: ( S

assume that

A7: S

A8: S

now :: thesis: y1 = y2end;

hence
y1 = y2
; :: 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;

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

then consider y, z being object such that

A9: f . x = [y,z] ;

y1 = [z,y] by A7, A9;

hence y1 = y2 by A8, A9; :: thesis: verum

end;A9: f . x = [y,z] ;

y1 = [z,y] by A7, A9;

hence y1 = y2 by A8, A9; :: thesis: verum

( dom g = dom f & ( for x being object st x in dom f holds

S