consider i being Element of I such that
A1: for j being Element of I st i <> j holds
B . j is 1 -element by Def20;
take i ; :: thesis:

now :: thesis:

assume A2: B . i is trivial ; :: thesis:
for S being set st S in rng B holds
S is trivial

proof

let S be set ; :: thesis:
assume S in rng B ; :: thesis:
then consider j being object such that
A3: j in dom B and
A4: S = B . j by FUNCT_1:def 3;
reconsider j = j as Element of I by A3, PARTFUN1:def 2;

per cases ;

suppose i = j ; :: thesis:

hence S is trivial by A2, A4; :: thesis:

end;

suppose i <> j ; :: thesis:

then B . j is 1 -element by A1;
hence S is trivial by A4; :: thesis:

end;

end;

end;

hence contradiction by Def16; :: thesis:

end;

hence not B . i is trivial ; :: thesis: