theorem Th21: :: MESFUN11:21

for X, Y being non empty set
for f being PartFunc of X,ExtREAL
for r being Real st f = Y --> r holds
( f is V120() & f is V121() )