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