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 :: thesis: for x, y being Element of Fin Y holds g . ((FinUnion Y) . (x,y)) = G . ((g . x),(g . y))
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 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; :: thesis: verum