let a, b be set ; :: thesis: Union (a,b followed_by {} ) = a \/ b
rng (a,b followed_by {} ) = {a,b,{} } by FUNCT_7:129;
hence Union (a,b followed_by {} ) = union {a,b} by MEASURE1:1
.= a \/ b by ZFMISC_1:93 ;
:: thesis: verum