let T1, T2 be LeftOperation of S,[: the carrier of S,Z:]; :: thesis: ( ( for s being Element of S holds T1 . s = the_left_translation_of (s,Z) ) & ( for s being Element of S holds T2 . s = the_left_translation_of (s,Z) ) implies T1 = T2 )
assume that
A24: for s being Element of S holds T1 . s = the_left_translation_of (s,Z) and
A25: for s being Element of S holds T2 . s = the_left_translation_of (s,Z) ; :: thesis: T1 = T2
let x be Element of S; :: according to FUNCT_2:def 8 :: thesis: ^ = ^
thus T1 . x = the_left_translation_of (x,Z) by A24
.= T2 . x by A25 ; :: thesis: verum