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