theorem Th5: :: SETWOP_2:5

for C, C9, D being non empty set
for B being Element of Fin C
for A being Element of Fin C9
for F being BinOp of D
for f being Function of C,D
for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds
F $$ (A,g) = F $$ (B,f)