let X be set ; :: thesis: for P being a_partition of X
for f being FinSequence of X ex p being FinSequence of P st f in product p
let P be a_partition of X; :: thesis: for f being FinSequence of X ex p being FinSequence of P st f in product p
let f be FinSequence of X; :: thesis: ex p being FinSequence of P st f in product p
A1: rng f c= X ;
union P = X by EQREL_1:def 4;
then consider p being Function such that
A2: dom p = dom f and
A3: rng p c= P and
A4: f in product p by A1, Th6;
dom p = Seg (len f) by A2, FINSEQ_1:def 3;
then p is FinSequence by FINSEQ_1:def 2;
then p is FinSequence of P by A3, FINSEQ_1:def 4;
hence ex p being FinSequence of P st f in product p by A4; :: thesis: verum