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
A17: for s being Element of S holds T1 . s = the_left_translation_of s,Z and
A18: 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 9 :: thesis: ^ = ^
thus T1 . x = the_left_translation_of x,Z by A17
.= T2 . x by A18 ; :: thesis: verum