theorem Th50: :: SETWISEO:53

for X, Z being non empty set
for Y being set
for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds
for f being Function of X,(Fin Y)
for g being Function of (Fin Y),Z st g . ({}. Y) = the_unity_wrt G & ( for x, y being Element of Fin Y holds g . (x \/ y) = G . ((g . x),(g . y)) ) holds
for B being Element of Fin X holds g . (FinUnion (B,f)) = G $$ (B,(g * f))