let I be set ; :: thesis: for A being ManySortedSet of I
for B being non-empty ManySortedSet of I holds A is_transformable_to B
let A be ManySortedSet of I; :: thesis: for B being non-empty ManySortedSet of I holds A is_transformable_to B
let B be non-empty ManySortedSet of I; :: thesis: A is_transformable_to B
for i being set st i in I & B . i = {} holds
A . i = {} ;
hence A is_transformable_to B by PZFMISC1:def 3; :: thesis: verum