let a be set ; :: according to PENCIL_1:def 16 :: thesis: ( a in rng {A} implies a is trivial )
assume a in rng {A} ; :: thesis: a is trivial
then consider i being set such that
A1: ( i in dom {A} & a = {A} . i ) by FUNCT_1:def 5;
dom {A} = I by PARTFUN1:def 4;
then a = {(A . i)} by A1, PZFMISC1:def 1;
hence a is trivial ; :: thesis: verum