let E be set ; :: thesis: for A, B being Subset of (E ^omega ) holds (A ? ) \/ (B ? ) = (A \/ B) ?
let A, B be Subset of (E ^omega ); :: thesis: (A ? ) \/ (B ? ) = (A \/ B) ?
thus (A \/ B) ? = {(<%> E)} \/ (A \/ B) by Th76
.= (A \/ {(<%> E)}) \/ (B \/ {(<%> E)}) by XBOOLE_1:5
.= (A ? ) \/ (B \/ {(<%> E)}) by Th76
.= (A ? ) \/ (B ? ) by Th76 ; :: thesis: verum