let X be non empty set ; for Y, Z being set
for f being Function of X,(Fin Y)
for g being Function of (Fin Y),(Fin Z) st g . ({}. Y) = {}. Z & ( for x, y being Element of Fin Y holds g . (x \/ y) = (g . x) \/ (g . y) ) holds
for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f))
let Y, Z be set ; for f being Function of X,(Fin Y)
for g being Function of (Fin Y),(Fin Z) st g . ({}. Y) = {}. Z & ( for x, y being Element of Fin Y holds g . (x \/ y) = (g . x) \/ (g . y) ) holds
for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f))
let f be Function of X,(Fin Y); for g being Function of (Fin Y),(Fin Z) st g . ({}. Y) = {}. Z & ( for x, y being Element of Fin Y holds g . (x \/ y) = (g . x) \/ (g . y) ) holds
for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f))
let g be Function of (Fin Y),(Fin Z); ( g . ({}. Y) = {}. Z & ( for x, y being Element of Fin Y holds g . (x \/ y) = (g . x) \/ (g . y) ) implies for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f)) )
assume that
A1:
g . ({}. Y) = {}. Z
and
A2:
for x, y being Element of Fin Y holds g . (x \/ y) = (g . x) \/ (g . y)
; for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f))
A3:
g . ({}. Y) = the_unity_wrt (FinUnion Z)
by A1, Th40;
let B be Element of Fin X; g . (FinUnion (B,f)) = FinUnion (B,(g * f))
A5:
FinUnion Z is idempotent
by Th34;
( FinUnion Z is associative & FinUnion Z is commutative )
by Th35, Th36;
hence
g . (FinUnion (B,f)) = FinUnion (B,(g * f))
by A5, A3, A4, Th38, Th50; verum