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