let I be non empty set ; :: thesis: for f, g being ManySortedSet of I holds dom <:f,g:> = I
let f, g be ManySortedSet of I; :: thesis: dom <:f,g:> = I
thus dom <:f,g:> = (dom f) /\ (dom g) by FUNCT_3:def 7
.= I /\ (dom g) by PARTFUN1:def 2
.= I /\ I by PARTFUN1:def 2
.= I ; :: thesis: verum