let A be set ; :: thesis: for x being object holds
( x in 1 -tuples_on A iff ex a being set st
( a in A & x = <*a*> ) )
let x be object ; :: thesis: ( x in 1 -tuples_on A iff ex a being set st
( a in A & x = <*a*> ) )

hereby :: thesis: ( ex a being set st
( a in A & x = <*a*> ) implies x in 1 -tuples_on A )

assume x in 1 -tuples_on A ; :: thesis: ex a being set st
( a in A & x = <*a*> )
then x in { s where s is Element of A * : len s = 1 } ;
then consider s being Element of A * such that
A1: x = s and
A2: len s = 1 ;
take a = s . 1; :: thesis: ( a in A & x = <*a*> )
A3: ( rng <*a*> = {a} & a in {a} ) by FINSEQ_1:39, TARSKI:def 1;
A4: rng s c= A by RELAT_1:def 19;
x = <*a*> by A1, A2, FINSEQ_1:40;
hence ( a in A & x = <*a*> ) by A1, A3, A4; :: thesis: verum

end;

given a being set such that A5: a in A and
A6: x = <*a*> ; :: thesis: x in 1 -tuples_on A
reconsider A = A as non empty set by A5;
reconsider a = a as Element of A by A5;
<*a*> is Element of 1 -tuples_on A by Th96;
hence x in 1 -tuples_on A by A6; :: thesis: verum