let A, a be set ; :: thesis: ( <*a*> in 1 -tuples_on A implies a in A )
assume <*a*> in 1 -tuples_on A ; :: thesis: a in A
then consider a' being set such that
A1: ( a' in A & <*a*> = <*a'*> ) by Th8;
( <*a*> . 1 = a & <*a'*> . 1 = a' ) by FINSEQ_1:57;
hence a in A by A1; :: thesis: verum