theorem Th21: :: HILBERT3:22

for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds
for f being Function of A,(Funcs (B,C)) holds dom (Frege f) = Funcs (A,B)