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)
A2: ( FinUnion Y is commutative & FinUnion Y is associative & FinUnion Y is idempotent ) by Th49, Th50, Th51;
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 A3: 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 A4: 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)

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 A4 ; :: thesis: verum

end;

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