hereby :: thesis: ( ( for i being set st i in rng F holds
i is non trivial 1-sorted ) implies F is non-Trivial-yielding )

assume A1: F is non-Trivial-yielding ; :: thesis: for i being set st i in rng F holds
i is non trivial 1-sorted
let i be set ; :: thesis: ( i in rng F implies i is non trivial 1-sorted )
assume A2: i in rng F ; :: thesis: i is non trivial 1-sorted
then ex x being set st
( x in dom F & i = F . x ) by FUNCT_1:def 3;
hence i is non trivial 1-sorted by A1, A2, Def17, PRALG_1:def 11; :: thesis: verum

end;

assume A3: for i being set st i in rng F holds
i is non trivial 1-sorted ; :: thesis: F is non-Trivial-yielding
let S be 1-sorted ; :: according to PENCIL_1:def 17 :: thesis: ( S in rng F implies not S is trivial )
thus ( S in rng F implies not S is trivial ) by A3; :: thesis: verum