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 Th61
.= union ((g * f) .: B) by RELAT_1:159
.= FinUnion B,(g * f) by Th61 ; :: thesis: verum