let X, Z be non empty set ; :: thesis: 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)
let Y be set ; :: thesis: 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)
let G be BinOp of Z; :: thesis: ( G is commutative & G is associative & G is idempotent & G is having_a_unity implies 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) )
assume A1: ( G is commutative & G is associative & G is idempotent & G is having_a_unity ) ; :: thesis: 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)
let f be Function of X,(Fin Y); :: thesis: 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)
let g be Function of (Fin Y),Z; :: thesis: ( g . ({}. Y) = the_unity_wrt G & ( for x, y being Element of Fin Y holds g . (x \/ y) = G . (g . x),(g . y) ) implies for B being Element of Fin X holds g . (FinUnion B,f) = G $$ B,(g * f) )
assume that
A2: g . ({}. Y) = the_unity_wrt G and
A3: for x, y being Element of Fin Y holds g . (x \/ y) = G . (g . x),(g . y) ; :: thesis: for B being Element of Fin X holds g . (FinUnion B,f) = G $$ B,(g * f)
let B be Element of Fin X; :: thesis: g . (FinUnion B,f) = G $$ B,(g * f)
A4: {} = {}. X ;
A5: {} = {}. (Fin Y) ;

per cases ( B = {} or B <> {} ) ;

suppose A6: B = {} ; :: thesis: g . (FinUnion B,f) = G $$ B,(g * f)

then A7: f .: B = {} by RELAT_1:149;
thus g . (FinUnion B,f) = g . ({}. Y) by A4, A6, Th59
.= G $$ (f .: B),g by A1, A2, A5, A7, Th40
.= G $$ B,(g * f) by A1, Th44 ; :: thesis: verum

end;

suppose B <> {} ; :: thesis: g . (FinUnion B,f) = G $$ B,(g * f)

hence g . (FinUnion B,f) = G $$ B,(g * f) by A1, A3, Th64; :: thesis: verum

end;

end;