let E be set ; :: thesis: for A being Subset of (E ^omega) holds A |^ (0,2) = ({(<%> E)} \/ A) \/ (A ^^ A)
let A be Subset of (E ^omega); :: thesis: A |^ (0,2) = ({(<%> E)} \/ A) \/ (A ^^ A)
thus A |^ (0,2) = (A |^ (0,1)) \/ (A |^ (1 + 1)) by Th26
.= ({(<%> E)} \/ A) \/ (A |^ (1 + 1)) by Th46
.= ({(<%> E)} \/ A) \/ (A ^^ A) by FLANG_1:26 ; :: thesis: verum