let D be set ; :: thesis: for F being FinSequence of D *
for i, j being Element of NAT st i in dom F & j in dom (F . i) holds
( (Sum (Card (F | (i -' 1)))) + j in dom (FlattenSeq F) & (F . i) . j = (FlattenSeq F) . ((Sum (Card (F | (i -' 1)))) + j) )
set F = <*> (D *);
defpred S₁[ FinSequence of D * ] means for i, j being Element of NAT st i in dom $1 & j in dom ($1 . i) holds
( (Sum (Card ($1 | (i -' 1)))) + j in dom (FlattenSeq $1) & ($1 . i) . j = (FlattenSeq $1) . ((Sum (Card ($1 | (i -' 1)))) + j) );
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: for i, j being Element of NAT st i in dom F & j in dom (F . i) holds
( (Sum (Card (F | (i -' 1)))) + j in dom (FlattenSeq F) & (F . i) . j = (FlattenSeq F) . ((Sum (Card (F | (i -' 1)))) + j) ) ; :: thesis: S₁[F ^ <*p*>]
let i, j be Element of NAT ; :: thesis: ( i in dom (F ^ <*p*>) & j in dom ((F ^ <*p*>) . i) implies ( (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>)) & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) ) )
assume that
A3: i in dom (F ^ <*p*>) and
A4: j in dom ((F ^ <*p*>) . i) ; :: thesis: ( (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>)) & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) )
A5: FlattenSeq (F ^ <*p*>) = (FlattenSeq F) ^ (FlattenSeq <*p*>) by Th21D
.= (FlattenSeq F) ^ p by Th13D ;

per cases ( not i in dom F or i in dom F ) ;

suppose A6: not i in dom F ; :: thesis: ( (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>)) & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) )

1 <= i by A3, FINSEQ_3:27;
then len F < i by A6, FINSEQ_3:27;
then A7: (len F) + 1 <= i by NAT_1:13;
A8: len (F ^ <*p*>) = (len F) + (len <*p*>) by FINSEQ_1:35
.= (len F) + 1 by FINSEQ_1:57 ;
i <= len (F ^ <*p*>) by A3, FINSEQ_3:27;
then A9: i = (len F) + 1 by A8, A7, XXREAL_0:1;
then i -' 1 = len F by NAT_D:34;
then A10: (F ^ <*p*>) | (i -' 1) = F by FINSEQ_5:26;
A11: Sum (Card F) = len (FlattenSeq F) by Th30;
1 in dom <*p*> by FINSEQ_5:6;
then A12: (F ^ <*p*>) . i = <*p*> . 1 by A9, FINSEQ_1:def 7
.= p by FINSEQ_1:57 ;
hence (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>)) by A4, A5, A10, A11, FINSEQ_1:41; :: thesis: ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j)
thus ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) by A4, A5, A12, A10, A11, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A13: i in dom F ; :: thesis: ( (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>)) & ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) )

then A14: j in dom (F . i) by A4, FINSEQ_1:def 7;
then A15: (Sum (Card (F | (i -' 1)))) + j in dom (FlattenSeq F) by A2, A13;
A16: i -' 1 <= i by NAT_D:35;
i <= len F by A13, FINSEQ_3:27;
then A17: (F ^ <*p*>) | (i -' 1) = F | (i -' 1) by A16, FINSEQ_5:25, XXREAL_0:2;
dom (FlattenSeq F) c= dom (FlattenSeq (F ^ <*p*>)) by A5, FINSEQ_1:39;
hence (Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>)) by A17, A15; :: thesis: ((F ^ <*p*>) . i) . j = (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j)
thus ((F ^ <*p*>) . i) . j = (F . i) . j by A13, FINSEQ_1:def 7
.= (FlattenSeq F) . ((Sum (Card (F | (i -' 1)))) + j) by A2, A13, A14
.= (FlattenSeq (F ^ <*p*>)) . ((Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j) by A5, A17, A15, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

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