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

A4: now

let x, y be Element of Fin Y; :: thesis: g . ((FinUnion Y) . x,y) = G . (g . x),(g . y)
thus g . ((FinUnion Y) . x,y) = g . (x \/ y) by Def4
.= G . (g . x),(g . y) by A3 ; :: thesis: verum

end;

A5: FinUnion Y is idempotent by Th49;
( FinUnion Y is commutative & FinUnion Y is associative ) by Th50, Th51;
hence g . (FinUnion B,f) = G $$ B,(g * f) by A1, A5, A2, A4, Th39; :: thesis: verum