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