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