let X be non empty set ; :: thesis: for A being set
for f being Function of X,(Fin A)
for B1, B2 being Element of Fin X holds FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f))
let A be set ; :: thesis: for f being Function of X,(Fin A)
for B1, B2 being Element of Fin X holds FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f))
let f be Function of X,(Fin A); :: thesis: for B1, B2 being Element of Fin X holds FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f))
let B1, B2 be Element of Fin X; :: thesis: FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f))
thus FinUnion ((B1 \/ B2),f) = union (f .: (B1 \/ B2)) by Th46
.= union ((f .: B1) \/ (f .: B2)) by RELAT_1:120
.= (union (f .: B1)) \/ (union (f .: B2)) by ZFMISC_1:78
.= (FinUnion (B1,f)) \/ (union (f .: B2)) by Th46
.= (FinUnion (B1,f)) \/ (FinUnion (B2,f)) by Th46 ; :: thesis: verum