let E be set ; :: thesis: for A being Subset of
for m, n being Nat holds (A ? ) ^^ (A |^ m,n) = (A |^ m,n) ^^ (A ? )
let A be Subset of ; :: thesis: for m, n being Nat holds (A ? ) ^^ (A |^ m,n) = (A |^ m,n) ^^ (A ? )
let m, n be Nat; :: thesis: (A ? ) ^^ (A |^ m,n) = (A |^ m,n) ^^ (A ? )
(A |^ 0 ,1) ^^ (A |^ m,n) = (A |^ m,n) ^^ (A |^ 0 ,1) by Th39;
then (A ? ) ^^ (A |^ m,n) = (A |^ m,n) ^^ (A |^ 0 ,1) by Th79;
hence (A ? ) ^^ (A |^ m,n) = (A |^ m,n) ^^ (A ? ) by Th79; :: thesis: verum