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 Th35;
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 by FINSEQ_2:36;

now

len (FlattenSeq f) = len vfl by FINSEQ_2:37;
hence A1: dom (FlattenSeq f) = dom vfl by FINSEQ_3:31; :: 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 (Card f) by CARD_3:def 2;
A3: dom F = (dom ((dom f) --> v)) /\ (dom f) by PBOOLE:def 24
.= (dom f) /\ (dom f) by FUNCOP_1:19
.= dom f ;
then A4: dom f = dom (Card F) by CARD_3:def 2;

now

let k be set ; :: thesis: ( k in dom f implies (Card f) . k = (Card F) . k )
assume A5: k in dom f ; :: thesis: (Card f) . k = (Card F) . k
then reconsider k1 = k as Element of NAT ;
A6: F . k = (((dom f) --> v) . k) * (f . k) by A3, A5, PBOOLE:def 24
.= v * (f . k) by A5, FUNCOP_1:13 ;
f . k1 in X * by A5, FINSEQ_2:13;
then reconsider fk = f . k as FinSequence of X by FINSEQ_1:def 11;
thus (Card f) . k = len fk by A5, CARD_3:def 2
.= len (F . k) by A6, FINSEQ_2:37
.= (Card F) . k by A3, A5, CARD_3:def 2 ; :: thesis: verum

end;

then A7: Card f = Card F by A2, A4, FUNCT_1:9;
then len (FlattenSeq f) = len (FlattenSeq F) by Th31;
hence dom (FlattenSeq f) = dom (FlattenSeq F) by FINSEQ_3:31; :: 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 Element of 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 Th32;
A13: dom v = X by FUNCT_2:def 1;
f . i in X * by A9, FINSEQ_2:13;
then f . i is FinSequence of X by FINSEQ_1:def 11;
then rng (f . i) c= dom v by A13, FINSEQ_1:def 4;
then A14: j in dom (v * (f . i)) by A10, RELAT_1:46;
A15: F . i = (((dom f) --> v) . i) * (f . i) by A3, A9, PBOOLE:def 24
.= v * (f . i) by A9, FUNCOP_1:13 ;
f . i in X * by A9, FINSEQ_2:13;
then reconsider fi = f . i as FinSequence of X by FINSEQ_1:def 11;
len fi = len (F . i) by A15, FINSEQ_2:37;
then A16: j in dom (F . i) by A10, FINSEQ_3:31;
Card (F | (i -' 1)) = Card (F | (Seg (i -' 1))) by FINSEQ_1:def 15
.= (Card f) | (Seg (i -' 1)) by A7, Th11
.= Card (f | (Seg (i -' 1))) by Th11
.= Card (f | (i -' 1)) by FINSEQ_1:def 15 ;
then (FlattenSeq F) . k = (F . i) . j by A3, A9, A11, A16, Th33
.= ((((dom f) --> v) . i) * (f . i)) . j by A3, A9, PBOOLE:def 24
.= (v * (f . i)) . j by A9, FUNCOP_1:13
.= v . ((f . i) . j) by A14, FUNCT_1:22 ;
hence vfl . k = (FlattenSeq F) . k by A1, A8, A12, FUNCT_1:22; :: thesis: verum

end;

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