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.


One more attempt. I forgot that in Mizar, Function of A,B already means a 
total (exactly quasi-total) Function, so what I had in mind above is 
called PartFunc of A,B . Less trivial example for Function (or PartFunc) 
of A,B, is e.g.: 

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