let X be non empty set ; :: thesis: 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 ; :: thesis: 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); :: thesis: 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); :: thesis: ( 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) ; :: thesis: 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, Th55;

A4: now

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

end;

let B be Element of Fin X; :: thesis: g . (FinUnion B,f) = FinUnion B,(g * f)
A5: FinUnion Z is idempotent by Th49;
( FinUnion Z is associative & FinUnion Z is commutative ) by Th50, Th51;
hence g . (FinUnion B,f) = FinUnion B,(g * f) by A5, A3, A4, Th53, Th65; :: thesis: verum