let I be non empty set ; :: thesis: for f, g being ManySortedSet of I holds dom (commute <*<:f,g:>*>) = I
let f, g be ManySortedSet of I; :: thesis: dom (commute <*<:f,g:>*>) = I
A1: dom <:f,g:> = I by Lm3;
thus dom (commute <*<:f,g:>*>) = proj2 (dom (uncurry <*<:f,g:>*>)) by FUNCT_5:23
.= proj2 (dom (uncurry {[1,<:f,g:>]})) by FINSEQ_1:def 5
.= proj2 (dom (uncurry (1 .--> <:f,g:>))) by FUNCT_4:82
.= proj2 (dom (uncurry ({1} --> <:f,g:>))) by FUNCOP_1:def 9
.= rng [:{1},(dom <:f,g:>):] by FUNCT_6:8
.= I by A1, RELAT_1:160 ; :: thesis: verum