let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat holds (A |^ m,n) ^^ (A + ) = (A + ) ^^ (A |^ m,n)
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat holds (A |^ m,n) ^^ (A + ) = (A + ) ^^ (A |^ m,n)
let m, n be Nat; :: thesis: (A |^ m,n) ^^ (A + ) = (A + ) ^^ (A |^ m,n)
thus (A |^ m,n) ^^ (A + ) = (A |^ m,n) ^^ (A |^.. 1) by Th50
.= (A |^.. 1) ^^ (A |^ m,n) by Th25
.= (A + ) ^^ (A |^ m,n) by Th50 ; :: thesis: verum