let UN be Universe; :: thesis: for u being Element of UN holds disjoint-union (u,u) = {[u,{{}}]}
let u be Element of UN; :: thesis: disjoint-union (u,u) = {[u,{{}}]}
disjoint-union (u,u) = u .--> {({} UN)} by FUNCT_4:81
.= {[u,{({} UN)}]} by FUNCT_4:82 ;
hence disjoint-union (u,u) = {[u,{{}}]} ; :: thesis: verum