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)
let B be Element of Fin X; :: thesis: g . (FinUnion B,f) = FinUnion B,(g * f)
A3: ( FinUnion Z is associative & FinUnion Z is commutative & FinUnion Z is idempotent & FinUnion Z is having_a_unity ) by Th49, Th50, Th51, Th53;
A4: g . ({}. Y) = the_unity_wrt (FinUnion Z) by A1, Th55;

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;

hence g . (FinUnion B,f) = FinUnion B,(g * f) by A3, A4, Th65; :: thesis: verum