hereby :: thesis: ( ( for x being set st x in I holds
X . x is trivial ) implies X is trivial-yielding )

assume A1: X is trivial-yielding ; :: thesis: for x being set st x in I holds
X . x is trivial
let x be set ; :: thesis: ( x in I implies X . x is trivial )
assume x in I ; :: thesis: X . x is trivial
then x in dom X by PARTFUN1:def 2;
then X . x in rng X by FUNCT_1:def 3;
hence X . x is trivial by A1, PENCIL_1:def 16; :: thesis: verum

end;

assume A2: for x being set st x in I holds
X . x is trivial ; :: thesis: X is trivial-yielding

now :: thesis: for y being set st y in rng X holds
y is trivial

let y be set ; :: thesis: ( y in rng X implies y is trivial )
assume y in rng X ; :: thesis: y is trivial
then consider x being object such that
A3: ( x in dom X & y = X . x ) by FUNCT_1:def 3;
thus y is trivial by A2, A3; :: thesis: verum

end;

hence X is trivial-yielding by PENCIL_1:def 16; :: thesis: verum