theorem Th20: :: HILBERT3:21

for A, B, C being set st ( B = {} implies A = {} ) & ( C = {} implies B = {} ) holds
for f being Function of A,(Funcs (B,C))
for g being Function of A,B holds rng (f .. g) c= C