let E be set ; :: thesis: for A being Subset of (E ^omega) holds A |^ 2 = A ^^ A
let A be Subset of (E ^omega); :: thesis: A |^ 2 = A ^^ A
thus A |^ 2 = A |^ (1 + 1)
.= (A |^ 1) ^^ A by Th24
.= A ^^ A by Th26 ; :: thesis: verum