let X be set ; :: thesis: for p being FinSequence of SmallestPartition X ex q being FinSequence of X st product p = {q}
set P = SmallestPartition X;
let p be FinSequence of SmallestPartition X; :: thesis: ex q being FinSequence of X st product p = {q}
consider q being Element of product p;
A1: dom q = dom p by CARD_3:18;
then reconsider q = q as FinSequence by Lm1;
A2: ( q in product p & product p c= Funcs (dom p),(Union p) ) by FUNCT_6:10;
then A3: ( q in Funcs (dom p),(Union p) & rng p c= SmallestPartition X & Union p = union (rng p) ) by CARD_3:def 4;
ex f being Function st
( q = f & dom f = dom p & rng f c= Union p ) by A2, FUNCT_2:def 2;
then ( rng q c= Union p & Union p c= union (SmallestPartition X) ) by A3, ZFMISC_1:95;
then ( rng q c= union (SmallestPartition X) & ( X = {} or X <> {} ) ) by XBOOLE_1:1;
then rng q c= X by EQREL_1:def 6;
then reconsider q = q as FinSequence of X by FINSEQ_1:def 4;
take q ; :: thesis: product p = {q}
thus product p c= {q} :: according to XBOOLE_0:def 10 :: thesis: {q} c= product p

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product p or x in {q} )
assume x in product p ; :: thesis: x in {q}
then consider g being Function such that
A4: ( x = g & dom g = dom p ) and
A5: for x being set st x in dom p holds
g . x in p . x by CARD_3:def 5;

now

let y be set ; :: thesis: ( y in dom p implies g . y = q . y )
assume y in dom p ; :: thesis: g . y = q . y
then A6: ( g . y in p . y & q . y in p . y & p . y in rng p ) by A5, CARD_3:18, FUNCT_1:def 5;
then A7: p . y in SmallestPartition X ;
reconsider X = X as non empty set by A6, EQREL_1:41;
SmallestPartition X = { {z} where z is Element of X : verum } by EQREL_1:46;
then consider z being Element of X such that
A8: p . y = {z} by A7;
thus g . y = z by A6, A8, TARSKI:def 1
.= q . y by A6, A8, TARSKI:def 1 ; :: thesis: verum

end;

then x = q by A1, A4, FUNCT_1:9;
hence x in {q} by TARSKI:def 1; :: thesis: verum

end;

thus {q} c= product p by ZFMISC_1:37; :: thesis: verum