:: deftheorem defines FuncZero LOPBAN_1:def 3 :
for X being set
for Y being non empty ZeroStr holds FuncZero (X,Y) = X --> (0. Y);