let E be set ; :: thesis: for A being Subset of (E ^omega) holds A |^ (2,2) = A ^^ A
let A be Subset of (E ^omega); :: thesis: A |^ (2,2) = A ^^ A
thus A |^ (2,2) = A |^ 2 by Th22
.= A ^^ A by FLANG_1:26 ; :: thesis: verum