let T1, T2 be LeftOperation of S,(the_subsets_of_card (n,E)); :: thesis: ( ( for s being Element of S holds T1 . s = the_extension_of_left_translation_of (n,s,LO) ) & ( for s being Element of S holds T2 . s = the_extension_of_left_translation_of (n,s,LO) ) implies T1 = T2 )
assume that
A13: for s being Element of S holds T1 . s = the_extension_of_left_translation_of (n,s,LO) and
A14: for s being Element of S holds T2 . s = the_extension_of_left_translation_of (n,s,LO) ; :: thesis: T1 = T2
let x be Element of S; :: according to FUNCT_2:def 8 :: thesis: ^ = ^
thus T1 . x = the_extension_of_left_translation_of (n,x,LO) by A13
.= T2 . x by A14 ; :: thesis: verum