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: S₁[ <*> (D * )] ;
A2: 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 A3: 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 ) )
assume A4: 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 ;
A5: FlattenSeq (F ^ <*p*>) = (FlattenSeq F) ^ (FlattenSeq <*p*>) by DTCONSTR:21
.= (FlattenSeq F) ^ p by DTCONSTR:13 ;
A6: Sum (Card F) = len (FlattenSeq F) by Th30;
A7: (F ^ <*p*>) | (len F) = F by FINSEQ_5:26;

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

suppose A8: 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 )
A9: Sum (Card ((F ^ <*p*>) | (i -' 1))) = len (FlattenSeq F) by A6, A7, NAT_D:34;
1 <= m by A4, FINSEQ_3:27;
then A10: len (FlattenSeq F) < m by A8, FINSEQ_3:27;
A11: len (F ^ <*p*>) = (len F) + (len <*p*>) by FINSEQ_1:35
.= (len F) + 1 by FINSEQ_1:56 ;
1 in dom <*p*> by FINSEQ_5:6;
then A12: (F ^ <*p*>) . i = <*p*> . 1 by FINSEQ_1:def 7
.= p by FINSEQ_1:57 ;
1 <= (len F) + 1 by NAT_1:11;
hence i in dom (F ^ <*p*>) by A11, FINSEQ_3:27; :: thesis: ( j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )
(len (FlattenSeq F)) + 1 <= m by A10, NAT_1:13;
then A13: 1 <= j by A9, NAT_D:55;
m <= len ((FlattenSeq F) ^ p) by A4, A5, FINSEQ_3:27;
then m <= (len (FlattenSeq F)) + (len p) by FINSEQ_1:35;
then j <= len p by A9, NAT_D:53;
hence A14: j in dom ((F ^ <*p*>) . i) by A12, A13, FINSEQ_3:27; :: 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 A9, A10, XREAL_1:237; :: thesis: ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k
hence ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k by A5, A9, A12, A14, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A15: 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
A16: i in dom F and
A17: j in dom (F . i) and
A18: k = (Sum (Card (F | (i -' 1)))) + j and
A19: (F . i) . j = (FlattenSeq F) . k by A3;
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:39;
hence i in dom (F ^ <*p*>) by A16; :: thesis: ( j in dom ((F ^ <*p*>) . i) & k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )
A20: (F ^ <*p*>) . i = F . i by A16, FINSEQ_1:def 7;
thus j in dom ((F ^ <*p*>) . i) by A16, A17, FINSEQ_1:def 7; :: thesis: ( k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k )
A21: i <= len F by A16, FINSEQ_3:27;
i -' 1 <= i by NAT_D:35;
hence k = (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j by A18, A21, FINSEQ_5:25, XXREAL_0:2; :: thesis: ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k
((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . m by A5, A15, A19, A20, FINSEQ_1:def 7;
hence ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . k ; :: thesis: verum

end;

end;

end;

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