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}
set q = the Element of product p;
A1: dom the Element of product p = dom p by CARD_3:9;
then reconsider q = the Element of product p as FinSequence by Lm1;
A2: q in product p ;
A3: product p c= Funcs ((dom p),(Union p)) by FUNCT_6:1;
A4: Union p = union (rng p) by CARD_3:def 4;
A5: ex f being Function st
( q = f & dom f = dom p & rng f c= Union p ) by A2, A3, FUNCT_2:def 2;
Union p c= union (SmallestPartition X) by A4, ZFMISC_1:77;
then rng q c= union (SmallestPartition X) by A5;
then rng q c= X by EQREL_1:def 4;
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 object ; :: 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
A6: x = g and
A7: dom g = dom p and
A8: for x being object st x in dom p holds
g . x in p . x by CARD_3:def 5;

now :: thesis: for y being object st y in dom p holds
g . y = q . y

let y be object ; :: thesis: ( y in dom p implies g . y = q . y )
assume A9: y in dom p ; :: thesis: g . y = q . y
then A10: g . y in p . y by A8;
A11: q . y in p . y by A9, CARD_3:9;
A12: p . y in rng p by A9, FUNCT_1:def 3;
then A13: p . y in SmallestPartition X ;
reconsider X = X as non empty set by A12;
SmallestPartition X = { {z} where z is Element of X : verum } by EQREL_1:37;
then consider z being Element of X such that
A14: p . y = {z} by A13;
thus g . y = z by A10, A14, TARSKI:def 1
.= q . y by A11, A14, TARSKI:def 1 ; :: thesis: verum

end;

then x = q by A1, A6, A7, FUNCT_1:2;
hence x in {q} by TARSKI:def 1; :: thesis: verum

end;

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