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