let X, Y be non empty set ; :: thesis: for f being FinSequence of X *
for v being Function of X,Y ex F being FinSequence of Y * st
( F = ((dom f) --> v) ** f & v * (FlattenSeq f) = FlattenSeq F )
let f be FinSequence of X * ; :: thesis: for v being Function of X,Y ex F being FinSequence of Y * st
( F = ((dom f) --> v) ** f & v * (FlattenSeq f) = FlattenSeq F )
let v be Function of X,Y; :: thesis: ex F being FinSequence of Y * st
( F = ((dom f) --> v) ** f & v * (FlattenSeq f) = FlattenSeq F )
reconsider F = ((dom f) --> v) ** f as FinSequence of Y * by Th30;
take F ; :: thesis: ( F = ((dom f) --> v) ** f & v * (FlattenSeq f) = FlattenSeq F )
thus F = ((dom f) --> v) ** f ; :: thesis: v * (FlattenSeq f) = FlattenSeq F
set Fl = FlattenSeq F;
set fl = FlattenSeq f;
reconsider vfl = v * (FlattenSeq f) as FinSequence of Y ;

now :: thesis: ( dom (FlattenSeq f) = dom vfl & dom (FlattenSeq f) = dom (FlattenSeq F) & ( for k being Nat st k in dom (FlattenSeq f) holds
vfl . k = (FlattenSeq F) . k ) )

len (FlattenSeq f) = len vfl by FINSEQ_2:33;
hence A1: dom (FlattenSeq f) = dom vfl by FINSEQ_3:29; :: thesis: ( dom (FlattenSeq f) = dom (FlattenSeq F) & ( for k being Nat st k in dom (FlattenSeq f) holds
vfl . k = (FlattenSeq F) . k ) )
A2: dom F = (dom ((dom f) --> v)) /\ (dom f) by PBOOLE:def 19
.= (dom f) /\ (dom f)
.= dom f ;

A3: now :: thesis: for k being object st k in dom f holds
(Card f) . k = (Card F) . k

let k be object ; :: thesis: ( k in dom f implies (Card f) . k = (Card F) . k )
assume A4: k in dom f ; :: thesis: (Card f) . k = (Card F) . k
then reconsider k1 = k as Element of NAT ;
A5: F . k = (((dom f) --> v) . k) * (f . k) by A2, A4, PBOOLE:def 19
.= v * (f . k) by A4, FUNCOP_1:7 ;
f . k1 in X * by A4, FINSEQ_2:11;
then reconsider fk = f . k as FinSequence of X by FINSEQ_1:def 11;
thus (Card f) . k = len fk by A4, CARD_3:def 2
.= len (F . k1) by A5, FINSEQ_2:33
.= (Card F) . k by A2, A4, CARD_3:def 2 ; :: thesis: verum

end;

A6: ( dom f = dom (Card f) & dom f = dom (Card F) ) by A2, CARD_3:def 2;
then A7: Card f = Card F by A3;
len (FlattenSeq f) = len (FlattenSeq F) by A6, A3, Th27, FUNCT_1:2;
hence dom (FlattenSeq f) = dom (FlattenSeq F) by FINSEQ_3:29; :: thesis: for k being Nat st k in dom (FlattenSeq f) holds
vfl . k = (FlattenSeq F) . k
let k be Nat; :: thesis: ( k in dom (FlattenSeq f) implies vfl . k = (FlattenSeq F) . k )
assume A8: k in dom (FlattenSeq f) ; :: thesis: vfl . k = (FlattenSeq F) . k
then consider i, j being Nat such that
A9: i in dom f and
A10: j in dom (f . i) and
A11: k = (Sum (Card (f | (i -' 1)))) + j and
A12: (f . i) . j = (FlattenSeq f) . k by Th28;
f . i in X * by A9, FINSEQ_2:11;
then reconsider fi = f . i as FinSequence of X by FINSEQ_1:def 11;
F . i = (((dom f) --> v) . i) * (f . i) by A2, A9, PBOOLE:def 19
.= v * (f . i) by A9, FUNCOP_1:7 ;
then len fi = len (F . i) by FINSEQ_2:33;
then A13: j in dom (F . i) by A10, FINSEQ_3:29;
f . i in X * by A9, FINSEQ_2:11;
then ( dom v = X & f . i is FinSequence of X ) by FINSEQ_1:def 11, FUNCT_2:def 1;
then rng (f . i) c= dom v by FINSEQ_1:def 4;
then A14: j in dom (v * (f . i)) by A10, RELAT_1:27;
Card (F | (i -' 1)) = Card (F | (Seg (i -' 1))) by FINSEQ_1:def 16
.= (Card f) | (Seg (i -' 1)) by A7, Th22
.= Card (f | (Seg (i -' 1))) by Th22
.= Card (f | (i -' 1)) by FINSEQ_1:def 16 ;
then (FlattenSeq F) . k = (F . i) . j by A2, A9, A11, A13, Th29
.= ((((dom f) --> v) . i) * (f . i)) . j by A2, A9, PBOOLE:def 19
.= (v * (f . i)) . j by A9, FUNCOP_1:7
.= v . ((f . i) . j) by A14, FUNCT_1:12 ;
hence vfl . k = (FlattenSeq F) . k by A1, A8, A12, FUNCT_1:12; :: thesis: verum

end;

hence v * (FlattenSeq f) = FlattenSeq F ; :: thesis: verum