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 idempotent & FinUnion A is commutative & FinUnion A is associative & FinUnion A is having_a_unity ) by Th49, Th50, Th51, Th53;
hence FinUnion ({}. X),f = the_unity_wrt (FinUnion A) by Th40
.= {} by Th55 ;
:: thesis: verum