let D be set ; 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 S1[ 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 S1[F] holds
S1[F ^ <*p*>]
proof
let F be
FinSequence of
D * ;
for p being Element of D * st S1[F] holds
S1[F ^ <*p*>]let p be
Element of
D * ;
( S1[F] implies S1[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) )
;
S1[F ^ <*p*>]
let i,
j be
Element of
NAT ;
( 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)
;
( (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 Th3
.=
(FlattenSeq F) ^ p
by Th1
;
per cases
( not i in dom F or i in dom F )
;
suppose A6:
not
i in dom F
;
( (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:25;
then
len F < i
by A6, FINSEQ_3:25;
then A7:
(len F) + 1
<= i
by NAT_1:13;
A8:
len (F ^ <*p*>) =
(len F) + (len <*p*>)
by FINSEQ_1:22
.=
(len F) + 1
by FINSEQ_1:40
;
i <= len (F ^ <*p*>)
by A3, FINSEQ_3:25;
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:23;
A11:
Sum (Card F) = len (FlattenSeq F)
by Th26;
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:40
;
hence
(Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>))
by A4, A5, A10, A11, FINSEQ_1:28;
((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;
verum end; suppose A13:
i in dom F
;
( (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:25;
then A17:
(F ^ <*p*>) | (i -' 1) = F | (i -' 1)
by A16, FINSEQ_5:22, XXREAL_0:2;
dom (FlattenSeq F) c= dom (FlattenSeq (F ^ <*p*>))
by A5, FINSEQ_1:26;
hence
(Sum (Card ((F ^ <*p*>) | (i -' 1)))) + j in dom (FlattenSeq (F ^ <*p*>))
by A17, A15;
((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
;
verum end; end;
end;
A18:
S1[ <*> (D *)]
;
thus
for F being FinSequence of D * holds S1[F]
from FINSEQ_2:sch 2(A18, A1); verum