Re: [mizar] Scheme for func definition with Fraenkel operator?

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Piotr,

>> Something related that _would_ be nice is to have "by"
>> strengthened in a way that:
>> 
>>   a in { x : P[x] } 
>> 
>> implies
>> 
>>   P[a]
>> 
>
>This can be syntactically incorrect in case 'a' is of an inappropriate type. 

That's true.  But often the type of a widens to the type of x.
I think I meant that case.

Freek