let A, X be non empty set ; 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 ; 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; ( 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 )
; 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; ( 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 <> {}
; 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); 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; ( ( 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))
; g . (FinUnion (B,f)) = G $$ (B,(g * f))
A5:
FinUnion Y is idempotent
by Th34;
( FinUnion Y is commutative & FinUnion Y is associative )
by Th35, Th36;
hence
g . (FinUnion (B,f)) = G $$ (B,(g * f))
by A1, A5, A2, A4, Th27; verum