let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for p being Permutation of I holds product J, product (J * p) are_homeomorphic
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for p being Permutation of I holds product J, product (J * p) are_homeomorphic
let p be Permutation of I; :: thesis: product J, product (J * p) are_homeomorphic
reconsider q = p " as Permutation of I ;

now :: thesis: for i being Element of I holds J . i,((J * p) * q) . i are_homeomorphic

let i be Element of I; :: thesis: J . i,((J * p) * q) . i are_homeomorphic
A1: J = J * (id (dom J)) by RELAT_1:52
.= J * (id I) by PARTFUN1:def 2
.= J * (p * q) by FUNCT_2:61
.= (J * p) * q by RELAT_1:36 ;
thus J . i,((J * p) * q) . i are_homeomorphic by A1; :: thesis: verum

end;

hence product J, product (J * p) are_homeomorphic by Th79; :: thesis: verum