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 that
A1: ( G is commutative & G is associative ) and
A2: G is idempotent and
A3: 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
A4: g . ({}. Y) = the_unity_wrt G and
A5: 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))
A6: {} = {}. X ;
A7: {} = {}. (Fin Y) ;