consider i being Element of I;
take i ; :: according to PENCIL_1:def 20 :: thesis: for j being Element of I st i <> j holds
( not {A} . j is empty & {A} . j is trivial )
let j be Element of I; :: thesis: ( i <> j implies ( not {A} . j is empty & {A} . j is trivial ) )
assume i <> j ; :: thesis: ( not {A} . j is empty & {A} . j is trivial )
{A} . j = {(A . j)} by PZFMISC1:def 1;
hence ( not {A} . j is empty & {A} . j is trivial ) ; :: thesis: verum