let E be set ; for A being Subset of (E ^omega)
for k, l, m, n being Nat holds (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))
let A be Subset of (E ^omega); for k, l, m, n being Nat holds (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))
let k, l, m, n be Nat; (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))