set E = [: the carrier of S,Z:];
set f = { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } ;

A1: now :: thesis: for x, y1, y2 being object st [x,y1] in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } & [x,y2] in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } holds
y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } & [x,y2] in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } implies y1 = y2 )
assume [x,y1] in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } ; :: thesis: ( [x,y2] in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } implies y1 = y2 )
then consider z19, z29 being Element of [: the carrier of S,Z:] such that
A2: [x,y1] = [z19,z29] and
A3: ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z19 = [s1,z] & z29 = [s2,z] ) ;
consider s19, s29 being Element of S, z9 being Element of Z such that
A4: s29 = s * s19 and
A5: z19 = [s19,z9] and
A6: z29 = [s29,z9] by A3;
assume [x,y2] in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } ; :: thesis: y1 = y2
then consider z199, z299 being Element of [: the carrier of S,Z:] such that
A7: [x,y2] = [z199,z299] and
A8: ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z199 = [s1,z] & z299 = [s2,z] ) ;
consider s199, s299 being Element of S, z99 being Element of Z such that
A9: s299 = s * s199 and
A10: z199 = [s199,z99] and
A11: z299 = [s299,z99] by A8;
x = z199 by A7, XTUPLE_0:1;
then [s19,z9] = [s199,z99] by A2, A5, A10, XTUPLE_0:1;
then ( s19 = s199 & z9 = z99 ) by XTUPLE_0:1;
hence y1 = y2 by A2, A4, A5, A6, A7, A9, A10, A11, XTUPLE_0:1; :: thesis: verum

end;

now :: thesis: for x being object st x in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } holds
ex y, z being object st x = [y,z]

let x be object ; :: thesis: ( x in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } implies ex y, z being object st x = [y,z] )
assume x in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } ; :: thesis: ex y, z being object st x = [y,z]
then consider z1, z2 being Element of [: the carrier of S,Z:] such that
A12: x = [z1,z2] and
ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ;
reconsider y = z1, z = z2 as object ;
take y = y; :: thesis: ex z being object st x = [y,z]
take z = z; :: thesis: x = [y,z]
thus x = [y,z] by A12; :: thesis: verum

end;

then reconsider f = { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } as Function by A1, FUNCT_1:def 1, RELAT_1:def 1;

now :: thesis: for x being object holds
( ( x in [: the carrier of S,Z:] implies ex y being object st [x,y] in f ) & ( ex y being object st [x,y] in f implies x in [: the carrier of S,Z:] ) )

let x be object ; :: thesis: ( ( x in [: the carrier of S,Z:] implies ex y being object st [x,y] in f ) & ( ex y being object st [x,y] in f implies x in [: the carrier of S,Z:] ) )

hereby :: thesis: ( ex y being object st [x,y] in f implies x in [: the carrier of S,Z:] )

assume x in [: the carrier of S,Z:] ; :: thesis: ex y being object st [x,y] in f
then consider s1, z being object such that
A13: s1 in the carrier of S and
A14: z in Z and
A15: x = [s1,z] by ZFMISC_1:def 2;
reconsider z = z as Element of Z by A14;
reconsider s1 = s1 as Element of S by A13;
set s2 = s * s1;
reconsider y = [(s * s1),z] as object ;
take y = y; :: thesis: [x,y] in f
x = [s1,z] by A15;
hence [x,y] in f ; :: thesis: verum

end;

given y being object such that A16: [x,y] in f ; :: thesis: x in [: the carrier of S,Z:]
consider z1, z2 being Element of [: the carrier of S,Z:] such that
A17: [x,y] = [z1,z2] and
ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) by A16;
x = z1 by A17, XTUPLE_0:1;
hence x in [: the carrier of S,Z:] ; :: thesis: verum

end;

then A18: dom f = [: the carrier of S,Z:] by XTUPLE_0:def 12;

now :: thesis: for y being object st y in rng f holds
y in [: the carrier of S,Z:]

let y be object ; :: thesis: ( y in rng f implies y in [: the carrier of S,Z:] )
assume y in rng f ; :: thesis: y in [: the carrier of S,Z:]
then consider x being object such that
A19: [x,y] in f by XTUPLE_0:def 13;
consider z1, z2 being Element of [: the carrier of S,Z:] such that
A20: [x,y] = [z1,z2] and
ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) by A19;
y = z2 by A20, XTUPLE_0:1;
hence y in [: the carrier of S,Z:] ; :: thesis: verum

end;

then rng f c= [: the carrier of S,Z:] ;
then reconsider f = f as Function of [: the carrier of S,Z:],[: the carrier of S,Z:] by A18, FUNCT_2:2;
take f ; :: thesis: for z1 being Element of [: the carrier of S,Z:] ex z2 being Element of [: the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st
( z2 = f . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] )
thus for z1 being Element of [: the carrier of S,Z:] ex z2 being Element of [: the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st
( z2 = f . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) :: thesis: verum

proof

let z1 be Element of [: the carrier of S,Z:]; :: thesis: ex z2 being Element of [: the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st
( z2 = f . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] )
set z2 = f . z1;
[z1,(f . z1)] in f by A18, FUNCT_1:1;
then consider z19, z29 being Element of [: the carrier of S,Z:] such that
A21: [z1,(f . z1)] = [z19,z29] and
A22: ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z19 = [s1,z] & z29 = [s2,z] ) ;
consider s1, s2 being Element of S, z being Element of Z such that
A23: ( s2 = s * s1 & z19 = [s1,z] & z29 = [s2,z] ) by A22;
take f . z1 ; :: thesis: ex s1, s2 being Element of S ex z being Element of Z st
( f . z1 = f . z1 & s2 = s * s1 & z1 = [s1,z] & f . z1 = [s2,z] )
take s1 ; :: thesis: ex s2 being Element of S ex z being Element of Z st
( f . z1 = f . z1 & s2 = s * s1 & z1 = [s1,z] & f . z1 = [s2,z] )
take s2 ; :: thesis: ex z being Element of Z st
( f . z1 = f . z1 & s2 = s * s1 & z1 = [s1,z] & f . z1 = [s2,z] )
take z ; :: thesis: ( f . z1 = f . z1 & s2 = s * s1 & z1 = [s1,z] & f . z1 = [s2,z] )
thus f . z1 = f . z1 ; :: thesis: ( s2 = s * s1 & z1 = [s1,z] & f . z1 = [s2,z] )
thus ( s2 = s * s1 & z1 = [s1,z] & f . z1 = [s2,z] ) by A21, A23, XTUPLE_0:1; :: thesis: verum

end;