:: deftheorem defines non-Trivial-yielding PENCIL_1:def 18 :
for F being 1-sorted-yielding Function holds
( F is non-Trivial-yielding iff for i being set st i in rng F holds
i is non trivial 1-sorted );