let IT1, IT2 be Function of [:the carrier of S,Z:],[:the carrier of S,Z:]; :: 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 = IT1 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) & ( 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 = IT2 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) implies IT1 = IT2 )
assume that
A15: 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 = IT1 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) and
A16: 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 = IT2 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ; :: thesis: IT1 = IT2
let x be Element of [:the carrier of S,Z:]; :: according to FUNCT_2:def 9 :: thesis: ^ = ^
consider z12 being Element of [:the carrier of S,Z:], s11, s12 being Element of S, z' being Element of Z such that
A17: ( z12 = IT1 . x & s12 = s * s11 & x = [s11,z'] & z12 = [s12,z'] ) by A15;
consider z22 being Element of [:the carrier of S,Z:], s21, s22 being Element of S, z'' being Element of Z such that
A18: ( z22 = IT2 . x & s22 = s * s21 & x = [s21,z''] & z22 = [s22,z''] ) by A16;
( s11 = s21 & z' = z'' ) by A17, A18, ZFMISC_1:33;
hence IT1 . x = IT2 . x by A17, A18; :: thesis: verum