let D be set ; :: thesis: for F being FinSequence of D *
for k being set st k in dom (FlattenSeq F) holds
ex i, j being Element of NAT st
( i in dom F & j in dom (F . i) & k = (Sum (Card (F | (i -' 1)))) + j & (F . i) . j = (FlattenSeq F) . k )
set F = <*> (D *);
defpred S₁[ FinSequence of D * ] means for k being set st k in dom (FlattenSeq $1) holds
ex i, j being Element of NAT st
( i in dom $1 & j in dom ($1 . i) & k = (Sum (Card ($1 | (i -' 1)))) + j & ($1 . i) . j = (FlattenSeq $1) . k );
A1: for F being FinSequence of D *
for p being Element of D * st S₁[F] holds
S₁[F ^ <*p*>]

proof

let F be FinSequence of D * ; :: thesis: for p being Element of D * st S₁[F] holds
S₁[F ^ <*p*>]
let p be Element of D * ; :: thesis: ( S₁[F] implies S₁[F ^ <*p*>] )
assume A2: S₁[F] ; :: thesis: S₁[F ^ <*p*>]
let k be set ; :: thesis: ( k in dom (FlattenSeq (F ^ <*p*>)) implies ex i, j being Element of NAT st
( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ) )
A3: FlattenSeq (F ^ <*p*>) = (FlattenSeq F) ^ (FlattenSeq <*p*>) by Th3
.= (FlattenSeq F) ^ p by Th1 ;
A4: ( Sum (Card F) = len (FlattenSeq F) & (F ^ <*p*>) | (len F) = F ) by Th27, FINSEQ_5:23;
assume A5: k in dom (FlattenSeq (F ^ <*p*>)) ; :: thesis: ex i, j being Element of NAT st
( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )
then reconsider m = k as Element of NAT ;

per cases ( not k in dom (FlattenSeq F) or k in dom (FlattenSeq F) ) ;

suppose A6: not k in dom (FlattenSeq F) ; :: thesis: ex i, j being Element of NAT st
( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )

take i = (len F) + 1; :: thesis: ex j being Element of NAT st
( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )
take j = m -' (Sum (Card ((F ^ <*p*>) | (i -' 1)))); :: thesis: ( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )
A7: 1 <= (len F) + 1 by NAT_1:11;
len (F ^ <*p*>) = (len F) + (len <*p*>) by FINSEQ_1:22
.= (len F) + 1 by FINSEQ_1:39 ;
hence i in dom (F ^ <*p*>) by A7, FINSEQ_3:25; :: thesis: ( j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )
A8: Sum (Card ((F ^ <*p*>) | (i -' 1))) = len (FlattenSeq F) by A4, NAT_D:34;
m <= len ((FlattenSeq F) ^ p) by A5, A3, FINSEQ_3:25;
then m <= (len (FlattenSeq F)) + (len p) by FINSEQ_1:22;
then A9: j <= len p by A8, NAT_D:53;
1 in dom <*p*> by FINSEQ_5:6;
then A10: (F ^ <*p*>) . i = <*p*> . 1 by FINSEQ_1:def 7
.= p by FINSEQ_1:40 ;
1 <= m by A5, FINSEQ_3:25;
then A11: len (FlattenSeq F) < m by A6, FINSEQ_3:25;
then (len (FlattenSeq F)) + 1 <= m by NAT_1:13;
then 1 <= j by A8, NAT_D:55;
hence A12: j in dom ((F ^ <*p*>) . i) by A10, A9, FINSEQ_3:25; :: thesis: ( k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )
thus k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j by A8, A11, XREAL_1:235; :: thesis: ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k
hence ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k by A3, A8, A10, A12, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A13: k in dom (FlattenSeq F) ; :: thesis: ex i, j being Element of NAT st
( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )

then consider i, j being Element of NAT such that
A14: i in dom F and
A15: j in dom (F . i) and
A16: k = (Sum (Card (F | (i -' 1)))) + j and
A17: (F . i) . j = (FlattenSeq F) . k by A2;
take i ; :: thesis: ex j being Element of NAT st
( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )
take j ; :: thesis: ( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )
dom F c= dom (F ^ <*p*>) by FINSEQ_1:26;
hence i in dom (F ^ <*p*>) by A14; :: thesis: ( j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )
thus j in dom ((F ^ <*p*>) . i) by A14, A15, FINSEQ_1:def 7; :: thesis: ( k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )
A18: i -' 1 <= i by NAT_D:35;
i <= len F by A14, FINSEQ_3:25;
hence k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j by A16, A18, FINSEQ_5:22, XXREAL_0:2; :: thesis: ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k
(F ^ <*p*>) . i = F . i by A14, FINSEQ_1:def 7;
hence ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k by A3, A13, A17, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

A19: S₁[ <*> (D *)] ;
thus for F being FinSequence of D * holds S₁[F] from FINSEQ_2:sch 2(A19, A1); :: thesis: verum