Dear Andrzej, >If a redefinition like > redefine func the carrier of H -> Subset of G >were allowed, the general redefinition of an element of a non empty >subset would work. But it is still not implemented. I see. Thanks for the answer! Freek