let E be set ; :: thesis: for A being Subset of (E ^omega) holds A |^ (1,2) = A \/ (A ^^ A)
let A be Subset of (E ^omega); :: thesis: A |^ (1,2) = A \/ (A ^^ A)
thus A |^ (1,2) = (A |^ 1) \/ (A |^ (1 + 1)) by Th28
.= A \/ (A |^ 2) by FLANG_1:25
.= A \/ (A ^^ A) by FLANG_1:26 ; :: thesis: verum