defpred S₁[ 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] ) );

A1: now :: thesis: for x being object st x in dom f holds
ex y being object st S₁[x,y]

let x be object ; :: thesis: ( x in dom f implies ex y being object st S₁[x,y] )
assume x in dom f ; :: thesis: ex y being object st S₁[x,y]

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] ) ) ) )

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

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] ) )

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] )

proof

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;

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

end;

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] ) )

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;

end;

end;

hence ex y being object st S₁[x,y] ; :: thesis: verum

end;

A6: now :: thesis: for x, y1, y2 being object st x in dom f & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

let x, y1, y2 be object ; :: thesis: ( x in dom f & S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
assume x in dom f ; :: thesis: ( S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
assume that
A7: S₁[x,y1] and
A8: S₁[x,y2] ; :: thesis: y1 = y2

now :: thesis: y1 = y2

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: 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;

suppose for y, z being object holds not f . x = [y,z] ; :: thesis: y1 = y2

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

end;

end;

end;

hence y1 = y2 ; :: thesis: verum

end;

thus ex g being Function st
( dom g = dom f & ( for x being object st x in dom f holds
S₁[x,g . x] ) ) from FUNCT_1:sch 2(A6, A1); :: thesis: verum