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