hereby :: thesis: ( ( for i being set st i in rng J holds
i is non empty 1-sorted ) implies J is yielding_non-empty_carriers )

assume A1: J is yielding_non-empty_carriers ; :: thesis: for i being set st i in rng J holds
i is non empty 1-sorted
let i be set ; :: thesis: ( i in rng J implies i is non empty 1-sorted )
assume A2: i in rng J ; :: thesis: i is non empty 1-sorted
then ex x being set st
( x in dom J & i = J . x ) by FUNCT_1:def 3;
hence i is non empty 1-sorted by A1, A2, PRALG_1:def 11, WAYBEL_3:def 7; :: thesis: verum

end;

assume A3: for i being set st i in rng J holds
i is non empty 1-sorted ; :: thesis: J is yielding_non-empty_carriers
let S be 1-sorted ; :: according to WAYBEL_3:def 7 :: thesis: ( not S in proj2 J or not S is empty )
thus ( not S in proj2 J or not S is empty ) by A3; :: thesis: verum