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 Th61
.= union ((f .: B1) \/ (f .: B2)) by RELAT_1:153
.= (union (f .: B1)) \/ (union (f .: B2)) by ZFMISC_1:96
.= (FinUnion B1,f) \/ (union (f .: B2)) by Th61
.= (FinUnion B1,f) \/ (FinUnion B2,f) by Th61 ; :: thesis: verum