let X, Y be non empty set ; :: thesis: for A being set
for B being Element of Fin X
for f being Function of X,Y
for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f))
let A be set ; :: thesis: for B being Element of Fin X
for f being Function of X,Y
for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f))
let B be Element of Fin X; :: thesis: for f being Function of X,Y
for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f))
let f be Function of X,Y; :: thesis: for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f))
let g be Function of Y,(Fin A); :: thesis: FinUnion ((f .: B),g) = FinUnion (B,(g * f))
thus FinUnion ((f .: B),g) = union (g .: (f .: B)) by Th46
.= union ((g * f) .: B) by RELAT_1:126
.= FinUnion (B,(g * f)) by Th46 ; :: thesis: verum