theorem Th121: :: FUNCT_2:122

for P being set
for B being non empty set holds Funcs (P,B) is FUNCTION_DOMAIN of P,B