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:27 ; :: thesis: verum