let E be set ; :: thesis: for A being Subset of (E ^omega) holds A ? = {(<%> E)} \/ A
let A be Subset of (E ^omega); :: thesis: A ? = {(<%> E)} \/ A
( A |^ 0 = {(<%> E)} & A |^ 1 = A ) by FLANG_1:24, FLANG_1:25;
hence A ? = {(<%> E)} \/ A by Th75; :: thesis: verum