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: not B . i is trivial

now :: thesis: not B . i is trivial

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

proof

let S be set ; :: thesis: ( S in rng B implies S is trivial )
assume S in rng B ; :: thesis: S is trivial
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 ( i = j or i <> j ) ;

suppose i = j ; :: thesis: S is trivial

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

end;

suppose i <> j ; :: thesis: S is trivial

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

end;

end;

end;

hence contradiction by Def16; :: thesis: verum

end;

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