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 ;

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

hence
product J, product (J * p) are_homeomorphic
by Th79; :: thesis: verumlet 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;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