defpred S₁[ set , set ] means ( ( for y, z being set st f . $1 = [y,z] holds
$2 = [z,y] ) & ( f . $1 = $2 or ex y, z being set st f . $1 = [y,z] ) );

A1: now

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

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 A2: ex y, z being set st f . x = [y,z] ; :: thesis: ex y1 being set st
( ( for y, z being set st f . x = [y,z] holds
y1 = [z,y] ) & ( f . x = y1 or ex y, z being set st f . x = [y,z] ) )

then consider y, z being set such that
A3: f . x = [y,z] ;
take y1 = [z,y]; :: thesis: ( ( for y, z being set st f . x = [y,z] holds
y1 = [z,y] ) & ( f . x = y1 or ex y, z being set st f . x = [y,z] ) )
thus for y, z being set st f . x = [y,z] holds
y1 = [z,y] :: thesis: ( f . x = y1 or ex y, z being set st f . x = [y,z] )

proof

let y9, z9 be set ; :: thesis: ( f . x = [y9,z9] implies y1 = [z9,y9] )
assume A4: f . x = [y9,z9] ; :: thesis: y1 = [z9,y9]
then z = z9 by A3, ZFMISC_1:27;
hence y1 = [z9,y9] by A3, A4, ZFMISC_1:27; :: thesis: verum

end;

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

end;

suppose A5: for y, z being set holds not f . x = [y,z] ; :: thesis: ex y1 being set st
( ( for y, z being set st f . x = [y,z] holds
y1 = [z,y] ) & ( f . x = y1 or ex y, z being set st f . x = [y,z] ) )

take y1 = f . x; :: thesis: ( ( for y, z being set st f . x = [y,z] holds
y1 = [z,y] ) & ( f . x = y1 or ex y, z being set st f . x = [y,z] ) )
thus ( ( for y, z being set st f . x = [y,z] holds
y1 = [z,y] ) & ( f . x = y1 or ex y, z being set st f . x = [y,z] ) ) by A5; :: thesis: verum

end;

end;

end;

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

end;

A6: now

let x, y1, y2 be set ; :: 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

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

then consider y, z being set 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 set 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 set st x in dom f holds
S₁[x,g . x] ) ) from FUNCT_1:sch 2(A6, A1); :: thesis: verum