theorem Th23: :: HILBERT3:24

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