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
A24: 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
A25: 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 8 :: thesis: ^ = ^
consider z12 being Element of [: the carrier of S,Z:], s11, s12 being Element of S, z9 being Element of Z such that
A26: ( z12 = IT1 . x & s12 = s * s11 ) and
A27: x = [s11,z9] and
A28: z12 = [s12,z9] by A24;
consider z22 being Element of [: the carrier of S,Z:], s21, s22 being Element of S, z99 being Element of Z such that
A29: ( z22 = IT2 . x & s22 = s * s21 ) and
A30: x = [s21,z99] and
A31: z22 = [s22,z99] by A25;
s11 = s21 by A27, A30, XTUPLE_0:1;
hence IT1 . x = IT2 . x by A26, A27, A28, A29, A30, A31, XTUPLE_0:1; :: thesis: verum