Re: [mizar] weak types

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

> surjective Function of A,B -> non empty Function of A,B;
> 
> (maybe A,B being non empty, I have just started enjoying ignoring
> the defaults for nonexistant cases :-)

Sorry, with B empty this is incorrect, so it would have to be:

let A be set;
let B be non empty set;
surjective Function of A,B -> non empty Function of A,B;

I still enjoy not caring about the emptiness of A.