let x be non empty set ; :: thesis: product <*x*> = { <*y*> where y is Element of x : verum }
A1: ( rng <*x*> = {x} & <*x*> . 1 = x ) by FINSEQ_1:38, FINSEQ_1:40;
then ( {} in rng <*x*> implies {} = x ) ;
then <*x*> is non-empty 1 -element FinSequence by RELAT_1:def 9;
hence product <*x*> = { <*y*> where y is Element of x : verum } by A1, Thm21; :: thesis: verum