let X be non empty set ; :: thesis: for A being set
for f being Function of X,(Fin A) holds FinUnion (({}. X),f) = {}
let A be set ; :: thesis: for f being Function of X,(Fin A) holds FinUnion (({}. X),f) = {}
let f be Function of X,(Fin A); :: thesis: FinUnion (({}. X),f) = {}
( FinUnion A is commutative & FinUnion A is associative ) by Th35, Th36;
hence FinUnion (({}. X),f) = the_unity_wrt (FinUnion A) by Th28, Th38
.= {} by Th40 ;
:: thesis: verum