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] ) } ;
set E = [:the carrier of S,Z:];

A1: now

let x, y1, y2 be set ; :: 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 z1', z2' being Element of [:the carrier of S,Z:] such that
A2: ( [x,y1] = [z1',z2'] & ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1' = [s1,z] & z2' = [s2,z] ) ) ;
consider s1', s2' being Element of S, z' being Element of Z such that
A3: ( s2' = s * s1' & z1' = [s1',z'] & z2' = [s2',z'] ) by A2;
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 z1'', z2'' being Element of [:the carrier of S,Z:] such that
A4: ( [x,y2] = [z1'',z2''] & ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1'' = [s1,z] & z2'' = [s2,z] ) ) ;
consider s1'', s2'' being Element of S, z'' being Element of Z such that
A5: ( s2'' = s * s1'' & z1'' = [s1'',z''] & z2'' = [s2'',z''] ) by A4;
( x = z1'' & y2 = z2'' ) by A4, ZFMISC_1:33;
then [s1',z'] = [s1'',z''] by A2, A3, A5, ZFMISC_1:33;
then ( s1' = s1'' & z' = z'' ) by ZFMISC_1:33;
hence y1 = y2 by A2, A3, A4, A5, ZFMISC_1:33; :: thesis: verum

end;

now

let x be set ; :: 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 set 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 set st x = [y,z]
then consider z1, z2 being Element of [:the carrier of S,Z:] such that
A6: ( x = [z1,z2] & 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 set ;
take y = y; :: thesis: ex z being set st x = [y,z]
take z = z; :: thesis: x = [y,z]
thus x = [y,z] by A6; :: 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

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

hereby :: thesis: ( ex y being set 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 set st [x,y] in f
then consider s1, z being set such that
A7: ( s1 in the carrier of S & z in Z & x = [s1,z] ) by ZFMISC_1:def 2;
reconsider s1 = s1 as Element of S by A7;
reconsider z = z as Element of Z by A7;
set s2 = s * s1;
reconsider y = [(s * s1),z] as set ;
take y = y; :: thesis: [x,y] in f
( s * s1 = s * s1 & x = [s1,z] & y = [(s * s1),z] ) by A7;
hence [x,y] in f ; :: thesis: verum

end;

given y being set such that A8: [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
A9: ( [x,y] = [z1,z2] & ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) by A8;
x = z1 by A9, ZFMISC_1:33;
hence x in [:the carrier of S,Z:] ; :: thesis: verum

end;

then A10: dom f = [:the carrier of S,Z:] by RELAT_1:def 4;

now

let y be set ; :: 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 set such that
A11: [x,y] in f by RELAT_1:def 5;
consider z1, z2 being Element of [:the carrier of S,Z:] such that
A12: ( [x,y] = [z1,z2] & ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) by A11;
y = z2 by A12, ZFMISC_1:33;
hence y in [:the carrier of S,Z:] ; :: thesis: verum

end;

then rng f c= [:the carrier of S,Z:] by TARSKI:def 3;
then reconsider f = f as Function of [:the carrier of S,Z:],[:the carrier of S,Z:] by A10, FUNCT_2:4;
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 A10, FUNCT_1:8;
then consider z1', z2' being Element of [:the carrier of S,Z:] such that
A13: ( [z1,(f . z1)] = [z1',z2'] & ex s1, s2 being Element of S ex z being Element of Z st
( s2 = s * s1 & z1' = [s1,z] & z2' = [s2,z] ) ) ;
consider s1, s2 being Element of S, z being Element of Z such that
A14: ( s2 = s * s1 & z1' = [s1,z] & z2' = [s2,z] ) by A13;
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 A13, A14, ZFMISC_1:33; :: thesis: verum

end;