WELLFND1:1
trybulec <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
A comment in OSALG_1:
:: REVISE:: WELLFND1:1 should be generalised to Relation and moved to
RELAT_1
The problem is that WELLFND1:1
theorem :: WELLFND1:1
for X being set, f, g being Function st f c= g & X c= dom f holds f|X
= g|X
is not true for Relations, e.g.
f = { [1,2] } g = {[1,2],[1,3]} X = {1}
So, I have removed the comment.
Regards,
Andrzej