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