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