let L be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r)
let p, q, r be sequence of L; :: thesis: (p *' q) *' r = p *' (q *' r)
now let i be
Element of
NAT ;
:: thesis: ((p *' q) *' r) . i = (p *' (q *' r)) . iconsider r1 being
FinSequence of the
carrier of
L such that A1:
len r1 = i + 1
and A2:
((p *' q) *' r) . i = Sum r1
and A3:
for
k being
Element of
NAT st
k in dom r1 holds
r1 . k = ((p *' q) . (k -' 1)) * (r . ((i + 1) -' k))
by Def11;
consider r2 being
FinSequence of the
carrier of
L such that A4:
len r2 = i + 1
and A5:
(p *' (q *' r)) . i = Sum r2
and A6:
for
k being
Element of
NAT st
k in dom r2 holds
r2 . k = (p . (k -' 1)) * ((q *' r) . ((i + 1) -' k))
by Def11;
deffunc H1(
Nat)
-> Element of
((2 + 1) -tuples_on NAT ) * =
(Decomp ($1 -' 1),2) ^^ ($1 |-> <*((i + 1) -' $1)*>);
consider f2 being
FinSequence of
((2 + 1) -tuples_on NAT ) * such that A7:
len f2 = i + 1
and A8:
for
k being
Nat st
k in dom f2 holds
f2 . k = H1(
k)
from FINSEQ_2:sch 1();
A9:
dom f2 = Seg (i + 1)
by A7, FINSEQ_1:def 3;
reconsider f2 =
f2 as
FinSequence of
(3 -tuples_on NAT ) * ;
deffunc H2(
Nat)
-> Element of
((1 + 2) -tuples_on NAT ) * =
(((i + 2) -' $1) |-> <*($1 -' 1)*>) ^^ (Decomp ((i + 1) -' $1),2);
consider g2 being
FinSequence of
((1 + 2) -tuples_on NAT ) * such that A10:
len g2 = i + 1
and A11:
for
k being
Nat st
k in dom g2 holds
g2 . k = H2(
k)
from FINSEQ_2:sch 1();
A12:
dom g2 = Seg (i + 1)
by A10, FINSEQ_1:def 3;
reconsider g2 =
g2 as
FinSequence of
(3 -tuples_on NAT ) * ;
deffunc H3(
Nat)
-> Element of the
carrier of
L * =
prodTuples p,
q,
r,
(f2 /. $1);
consider f1 being
FinSequence of the
carrier of
L * such that A13:
len f1 = len f2
and A14:
for
k being
Nat st
k in dom f1 holds
f1 . k = H3(
k)
from FINSEQ_2:sch 1();
A15:
dom f1 = Seg (len f2)
by A13, FINSEQ_1:def 3;
deffunc H4(
Nat)
-> Element of the
carrier of
L * =
prodTuples p,
q,
r,
(g2 /. $1);
consider g1 being
FinSequence of the
carrier of
L * such that A16:
len g1 = len g2
and A17:
for
k being
Nat st
k in dom g1 holds
g1 . k = H4(
k)
from FINSEQ_2:sch 1();
A18:
dom g1 = Seg (len g2)
by A16, FINSEQ_1:def 3;
A19:
len (Sum f1) = i + 1
by A7, A13, MATRLIN:def 8;
X:
dom r1 = Seg (i + 1)
by A1, FINSEQ_1:def 3;
now let j be
Nat;
:: thesis: ( j in dom r1 implies r1 . j = (Sum f1) . j )assume A20:
j in dom r1
;
:: thesis: r1 . j = (Sum f1) . jthen A21:
j in dom r1
;
len f1 = len (Sum f1)
by MATRLIN:def 8;
then A22:
dom f1 = dom (Sum f1)
by FINSEQ_3:31;
A23:
dom r1 = dom f1
by A1, A7, A13, FINSEQ_3:31;
A24:
dom f1 = dom f2
by A13, FINSEQ_3:31;
consider r3 being
FinSequence of the
carrier of
L such that A25:
len r3 = (j -' 1) + 1
and A26:
(p *' q) . (j -' 1) = Sum r3
and A27:
for
k being
Element of
NAT st
k in dom r3 holds
r3 . k = (p . (k -' 1)) * (q . (((j -' 1) + 1) -' k))
by Def11;
A28:
f1 /. j =
f1 . j
by A21, A23, PARTFUN1:def 8
.=
prodTuples p,
q,
r,
(f2 /. j)
by A7, A14, A20, A15, X
;
A29:
( 1
<= j &
j <= i + 1 )
by A20, X, FINSEQ_1:3;
len (Decomp (j -' 1),2) =
(j -' 1) + 1
by Th9
.=
j
by A29, XREAL_1:237
;
then A30:
dom (Decomp (j -' 1),2) = Seg j
by FINSEQ_1:def 3;
A31:
dom (j |-> <*((i + 1) -' j)*>) = Seg j
by FUNCOP_1:19;
A32:
f2 /. j =
f2 . j
by A21, A23, A24, PARTFUN1:def 8
.=
(Decomp (j -' 1),2) ^^ (j |-> <*((i + 1) -' j)*>)
by A8, A20, A9, X
;
then A33:
dom (f2 /. j) =
(dom (Decomp (j -' 1),2)) /\ (dom (j |-> <*((i + 1) -' j)*>))
by MATRLIN:def 2
.=
Seg j
by A30, A31
;
A34:
len (prodTuples p,q,r,(f2 /. j)) =
len (f2 /. j)
by Def5
.=
j
by A20, A33, FINSEQ_1:def 3
;
A35:
dom (r3 * (r . ((i + 1) -' j))) = dom r3
by POLYNOM1:def 3;
then A36:
len (r3 * (r . ((i + 1) -' j))) = len r3
by FINSEQ_3:31;
A37:
len r3 = j
by A25, A29, XREAL_1:237;
X:
dom (prodTuples p,q,r,(f2 /. j)) = Seg j
by A34, FINSEQ_1:def 3;
now let k be
Nat;
:: thesis: ( k in dom (prodTuples p,q,r,(f2 /. j)) implies (prodTuples p,q,r,(f2 /. j)) . k = (r3 * (r . ((i + 1) -' j))) . k )assume A38:
k in dom (prodTuples p,q,r,(f2 /. j))
;
:: thesis: (prodTuples p,q,r,(f2 /. j)) . k = (r3 * (r . ((i + 1) -' j))) . kthen A39:
k in dom r3
by A37, X, FINSEQ_1:def 3;
then A40:
r3 /. k =
r3 . k
by PARTFUN1:def 8
.=
(p . (k -' 1)) * (q . (((j -' 1) + 1) -' k))
by A27, A39
;
A41:
(f2 /. j) /. k =
(f2 /. j) . k
by A33, A38, X, PARTFUN1:def 8
.=
((Decomp (j -' 1),2) . k) ^ ((j |-> <*((i + 1) -' j)*>) . k)
by A32, A33, A38, X, MATRLIN:def 2
.=
<*(k -' 1),(((j -' 1) + 1) -' k)*> ^ ((j |-> <*((i + 1) -' j)*>) . k)
by A25, A37, A38, Th14, X
.=
<*(k -' 1),(((j -' 1) + 1) -' k)*> ^ <*((i + 1) -' j)*>
by A38, X, FUNCOP_1:13
.=
<*(k -' 1),(((j -' 1) + 1) -' k),((i + 1) -' j)*>
by FINSEQ_1:60
;
( 1
in Seg 3 & 2
in Seg 3 & 3
in Seg 3 )
by ENUMSET1:def 1, FINSEQ_3:1;
then
( 1
in Seg (len ((f2 /. j) /. k)) & 2
in Seg (len ((f2 /. j) /. k)) & 3
in Seg (len ((f2 /. j) /. k)) )
by A41, FINSEQ_1:62;
then A42:
( 1
in dom ((f2 /. j) /. k) & 2
in dom ((f2 /. j) /. k) & 3
in dom ((f2 /. j) /. k) )
by FINSEQ_1:def 3;
then A43:
((f2 /. j) /. k) /. 1 =
((f2 /. j) /. k) . 1
by PARTFUN1:def 8
.=
k -' 1
by A41, FINSEQ_1:62
;
A44:
((f2 /. j) /. k) /. 2 =
((f2 /. j) /. k) . 2
by A42, PARTFUN1:def 8
.=
((j -' 1) + 1) -' k
by A41, FINSEQ_1:62
;
A45:
((f2 /. j) /. k) /. 3 =
((f2 /. j) /. k) . 3
by A42, PARTFUN1:def 8
.=
(i + 1) -' j
by A41, FINSEQ_1:62
;
thus (prodTuples p,q,r,(f2 /. j)) . k =
((p . (((f2 /. j) /. k) /. 1)) * (q . (((f2 /. j) /. k) /. 2))) * (r . (((f2 /. j) /. k) /. 3))
by A33, A38, Def5, X
.=
(r3 * (r . ((i + 1) -' j))) /. k
by A39, A40, A43, A44, A45, POLYNOM1:def 3
.=
(r3 * (r . ((i + 1) -' j))) . k
by A35, A39, PARTFUN1:def 8
;
:: thesis: verum end; then A46:
prodTuples p,
q,
r,
(f2 /. j) = r3 * (r . ((i + 1) -' j))
by A34, A36, A37, FINSEQ_2:10;
((p *' q) . (j -' 1)) * (r . ((i + 1) -' j)) = Sum (r3 * (r . ((i + 1) -' j)))
by A26, POLYNOM1:29;
hence r1 . j =
Sum (r3 * (r . ((i + 1) -' j)))
by A3, A21
.=
(Sum f1) /. j
by A21, A22, A23, A28, A46, MATRLIN:def 8
.=
(Sum f1) . j
by A21, A22, A23, PARTFUN1:def 8
;
:: thesis: verum end; then
r1 = Sum f1
by A1, A19, FINSEQ_2:10;
then A47:
Sum r1 = Sum (FlattenSeq f1)
by POLYNOM1:34;
A48:
len (Sum g1) = i + 1
by A10, A16, MATRLIN:def 8;
X:
dom r2 = Seg (i + 1)
by A4, FINSEQ_1:def 3;
now let j be
Nat;
:: thesis: ( j in dom r2 implies r2 . j = (Sum g1) . j )assume A49:
j in dom r2
;
:: thesis: r2 . j = (Sum g1) . jthen A50:
j in dom r2
;
len g1 = len (Sum g1)
by MATRLIN:def 8;
then A51:
dom g1 = dom (Sum g1)
by FINSEQ_3:31;
A52:
dom r2 = dom g1
by A4, A10, A16, FINSEQ_3:31;
A53:
dom g1 = dom g2
by A16, FINSEQ_3:31;
consider r3 being
FinSequence of the
carrier of
L such that A54:
len r3 = ((i + 1) -' j) + 1
and A55:
(q *' r) . ((i + 1) -' j) = Sum r3
and A56:
for
k being
Element of
NAT st
k in dom r3 holds
r3 . k = (q . (k -' 1)) * (r . ((((i + 1) -' j) + 1) -' k))
by Def11;
A57:
g1 /. j =
g1 . j
by A50, A52, PARTFUN1:def 8
.=
prodTuples p,
q,
r,
(g2 /. j)
by A10, A17, A49, A18, X
;
A58:
j <= i + 1
by A49, X, FINSEQ_1:3;
then A59:
(i + 1) - j >= 0
by XREAL_1:50;
(i + 1) + 1
>= i + 1
by NAT_1:11;
then
(i + 1) + 1
>= j
by A58, XXREAL_0:2;
then A60:
(i + 2) - j >= 0
by XREAL_1:50;
A61:
((i + 1) -' j) + 1 =
((i + 1) - j) + 1
by A59, XREAL_0:def 2
.=
(i + 2) -' j
by A60, XREAL_0:def 2
;
then
len (Decomp ((i + 1) -' j),2) = (i + 2) -' j
by Th9;
then A62:
dom (Decomp ((i + 1) -' j),2) = Seg ((i + 2) -' j)
by FINSEQ_1:def 3;
A63:
dom (((i + 2) -' j) |-> <*(j -' 1)*>) = Seg ((i + 2) -' j)
by FUNCOP_1:19;
A64:
g2 /. j =
g2 . j
by A50, A52, A53, PARTFUN1:def 8
.=
(((i + 2) -' j) |-> <*(j -' 1)*>) ^^ (Decomp ((i + 1) -' j),2)
by A11, A49, A12, X
;
then A65:
dom (g2 /. j) =
(dom (((i + 2) -' j) |-> <*(j -' 1)*>)) /\ (dom (Decomp ((i + 1) -' j),2))
by MATRLIN:def 2
.=
Seg ((i + 2) -' j)
by A62, A63
;
A66:
len (prodTuples p,q,r,(g2 /. j)) =
len (g2 /. j)
by Def5
.=
(i + 2) -' j
by A65, FINSEQ_1:def 3
;
A67:
dom ((p . (j -' 1)) * r3) = dom r3
by POLYNOM1:def 2;
then A68:
len ((p . (j -' 1)) * r3) = len r3
by FINSEQ_3:31;
X:
dom (prodTuples p,q,r,(g2 /. j)) = Seg ((i + 2) -' j)
by A66, FINSEQ_1:def 3;
now let k be
Nat;
:: thesis: ( k in dom (prodTuples p,q,r,(g2 /. j)) implies (prodTuples p,q,r,(g2 /. j)) . k = ((p . (j -' 1)) * r3) . k )assume A69:
k in dom (prodTuples p,q,r,(g2 /. j))
;
:: thesis: (prodTuples p,q,r,(g2 /. j)) . k = ((p . (j -' 1)) * r3) . kthen A70:
k in dom r3
by A54, A61, X, FINSEQ_1:def 3;
then A71:
r3 /. k =
r3 . k
by PARTFUN1:def 8
.=
(q . (k -' 1)) * (r . ((((i + 1) -' j) + 1) -' k))
by A56, A70
;
A72:
(g2 /. j) /. k =
(g2 /. j) . k
by A65, A69, X, PARTFUN1:def 8
.=
((((i + 2) -' j) |-> <*(j -' 1)*>) . k) ^ ((Decomp ((i + 1) -' j),2) . k)
by A64, A65, A69, X, MATRLIN:def 2
.=
((((i + 2) -' j) |-> <*(j -' 1)*>) . k) ^ <*(k -' 1),((((i + 1) -' j) + 1) -' k)*>
by A61, A69, Th14, X
.=
<*(j -' 1)*> ^ <*(k -' 1),((((i + 1) -' j) + 1) -' k)*>
by A69, X, FUNCOP_1:13
.=
<*(j -' 1),(k -' 1),((((i + 1) -' j) + 1) -' k)*>
by FINSEQ_1:60
;
( 1
in Seg 3 & 2
in Seg 3 & 3
in Seg 3 )
by ENUMSET1:def 1, FINSEQ_3:1;
then
( 1
in Seg (len ((g2 /. j) /. k)) & 2
in Seg (len ((g2 /. j) /. k)) & 3
in Seg (len ((g2 /. j) /. k)) )
by A72, FINSEQ_1:62;
then A73:
( 1
in dom ((g2 /. j) /. k) & 2
in dom ((g2 /. j) /. k) & 3
in dom ((g2 /. j) /. k) )
by FINSEQ_1:def 3;
then A74:
((g2 /. j) /. k) /. 1 =
((g2 /. j) /. k) . 1
by PARTFUN1:def 8
.=
j -' 1
by A72, FINSEQ_1:62
;
A75:
((g2 /. j) /. k) /. 2 =
((g2 /. j) /. k) . 2
by A73, PARTFUN1:def 8
.=
k -' 1
by A72, FINSEQ_1:62
;
A76:
((g2 /. j) /. k) /. 3 =
((g2 /. j) /. k) . 3
by A73, PARTFUN1:def 8
.=
(((i + 1) -' j) + 1) -' k
by A72, FINSEQ_1:62
;
thus (prodTuples p,q,r,(g2 /. j)) . k =
((p . (((g2 /. j) /. k) /. 1)) * (q . (((g2 /. j) /. k) /. 2))) * (r . (((g2 /. j) /. k) /. 3))
by A65, A69, Def5, X
.=
(p . (((g2 /. j) /. k) /. 1)) * ((q . (((g2 /. j) /. k) /. 2)) * (r . (((g2 /. j) /. k) /. 3)))
by GROUP_1:def 4
.=
((p . (j -' 1)) * r3) /. k
by A70, A71, A74, A75, A76, POLYNOM1:def 2
.=
((p . (j -' 1)) * r3) . k
by A67, A70, PARTFUN1:def 8
;
:: thesis: verum end; then A77:
prodTuples p,
q,
r,
(g2 /. j) = (p . (j -' 1)) * r3
by A54, A61, A66, A68, FINSEQ_2:10;
(p . (j -' 1)) * ((q *' r) . ((i + 1) -' j)) = Sum ((p . (j -' 1)) * r3)
by A55, POLYNOM1:28;
hence r2 . j =
Sum ((p . (j -' 1)) * r3)
by A6, A50
.=
(Sum g1) /. j
by A50, A51, A52, A57, A77, MATRLIN:def 8
.=
(Sum g1) . j
by A50, A51, A52, PARTFUN1:def 8
;
:: thesis: verum end; then
r2 = Sum g1
by A4, A48, FINSEQ_2:10;
then A78:
Sum r2 = Sum (FlattenSeq g1)
by POLYNOM1:34;
A79:
(
dom (Card f1) = dom f1 &
dom (Card f2) = dom f2 )
by CARD_3:def 2;
then A80:
(
len (Card f1) = len f1 &
len (Card f2) = len f2 )
by FINSEQ_3:31;
then X:
dom (Card f2) = Seg (i + 1)
by A7, FINSEQ_1:def 3;
now let j be
Nat;
:: thesis: ( j in dom (Card f2) implies (Card f2) . j = (Card f1) . j )assume A81:
j in dom (Card f2)
;
:: thesis: (Card f2) . j = (Card f1) . jthen A82:
(
j in dom f1 &
j in dom f2 )
by A7, A13, X, FINSEQ_1:def 3;
f1 . j = prodTuples p,
q,
r,
(f2 /. j)
by A7, A14, A81, A15, X;
then A83:
len (f1 . j) =
len (f2 /. j)
by Def5
.=
len (f2 . j)
by A82, PARTFUN1:def 8
;
thus (Card f2) . j =
len (f2 . j)
by A82, CARD_3:def 2
.=
(Card f1) . j
by A82, A83, CARD_3:def 2
;
:: thesis: verum end; then A84:
Card f2 = Card f1
by A13, A80, FINSEQ_2:10;
then A85:
len (FlattenSeq f1) = len (FlattenSeq f2)
by POLYNOM1:31;
then A86:
len (FlattenSeq f1) = len (prodTuples p,q,r,(FlattenSeq f2))
by Def5;
A87:
Seg (len (FlattenSeq f2)) = dom (FlattenSeq f2)
by FINSEQ_1:def 3;
X:
Seg (len (FlattenSeq f1)) = dom (FlattenSeq f1)
by FINSEQ_1:def 3;
now let j be
Nat;
:: thesis: ( j in dom (FlattenSeq f1) implies (FlattenSeq f1) . j = (prodTuples p,q,r,(FlattenSeq f2)) . j )assume A88:
j in dom (FlattenSeq f1)
;
:: thesis: (FlattenSeq f1) . j = (prodTuples p,q,r,(FlattenSeq f2)) . jthen
j in dom (FlattenSeq f1)
;
then consider i1,
j1 being
Element of
NAT such that A89:
i1 in dom f1
and A90:
j1 in dom (f1 . i1)
and A91:
j = (Sum (Card (f1 | (i1 -' 1)))) + j1
and A92:
(f1 . i1) . j1 = (FlattenSeq f1) . j
by POLYNOM1:32;
A93:
i1 in Seg (len f2)
by A13, A89, FINSEQ_1:def 3;
then A94:
f1 . i1 = prodTuples p,
q,
r,
(f2 /. i1)
by A14, A15;
A95:
i1 in dom f2
by A93, FINSEQ_1:def 3;
len (f1 . i1) =
len (f2 /. i1)
by A94, Def5
.=
len (f2 . i1)
by A79, A84, A89, PARTFUN1:def 8
;
then
j1 in Seg (len (f2 . i1))
by A90, FINSEQ_1:def 3;
then A96:
j1 in Seg (len (f2 /. i1))
by A95, PARTFUN1:def 8;
then A97:
j1 in dom (f2 /. i1)
by FINSEQ_1:def 3;
A98:
Seg (len (f2 /. i1)) = dom (f2 /. i1)
by FINSEQ_1:def 3;
A99:
j in dom (FlattenSeq f2)
by A85, A88, A87, FINSEQ_1:def 3;
then consider i2,
j2 being
Element of
NAT such that A100:
i2 in dom f2
and A101:
j2 in dom (f2 . i2)
and A102:
j = (Sum (Card (f2 | (i2 -' 1)))) + j2
and A103:
(f2 . i2) . j2 = (FlattenSeq f2) . j
by POLYNOM1:32;
(Sum ((Card f1) | (i1 -' 1))) + j1 =
(Sum (Card (f1 | (i1 -' 1)))) + j1
by Th16
.=
(Sum ((Card f2) | (i2 -' 1))) + j2
by A91, A102, Th16
;
then A104:
(
i1 = i2 &
j1 = j2 )
by A84, A89, A90, A100, A101, Th22;
A105:
(f2 /. i1) /. j1 =
(f2 /. i1) . j1
by A97, PARTFUN1:def 8
.=
(f2 . i1) . j1
by A95, PARTFUN1:def 8
.=
(FlattenSeq f2) /. j
by A99, A103, A104, PARTFUN1:def 8
;
thus (FlattenSeq f1) . j =
((p . (((f2 /. i1) /. j1) /. 1)) * (q . (((f2 /. i1) /. j1) /. 2))) * (r . (((f2 /. i1) /. j1) /. 3))
by A92, A94, A96, A98, Def5
.=
((p . (((FlattenSeq f2) /. j) /. 1)) * (q . (((FlattenSeq f2) /. j) /. 2))) * (r . (((FlattenSeq f2) /. j) /. 3))
by A105
.=
(prodTuples p,q,r,(FlattenSeq f2)) . j
by A85, A87, A88, Def5, X
;
:: thesis: verum end; then A106:
FlattenSeq f1 = prodTuples p,
q,
r,
(FlattenSeq f2)
by A86, FINSEQ_2:10;
A107:
(
dom (Card g1) = dom g1 &
dom (Card g2) = dom g2 )
by CARD_3:def 2;
then A108:
(
len (Card g1) = len g1 &
len (Card g2) = len g2 )
by FINSEQ_3:31;
then X:
dom (Card g2) = Seg (i + 1)
by A10, FINSEQ_1:def 3;
now let j be
Nat;
:: thesis: ( j in dom (Card g2) implies (Card g2) . j = (Card g1) . j )assume A109:
j in dom (Card g2)
;
:: thesis: (Card g2) . j = (Card g1) . jthen A110:
(
j in dom g1 &
j in dom g2 )
by A10, A16, X, FINSEQ_1:def 3;
g1 . j = prodTuples p,
q,
r,
(g2 /. j)
by A10, A17, A109, A18, X;
then A111:
len (g1 . j) =
len (g2 /. j)
by Def5
.=
len (g2 . j)
by A110, PARTFUN1:def 8
;
thus (Card g2) . j =
len (g2 . j)
by A110, CARD_3:def 2
.=
(Card g1) . j
by A110, A111, CARD_3:def 2
;
:: thesis: verum end; then A112:
Card g2 = Card g1
by A16, A108, FINSEQ_2:10;
then A113:
len (FlattenSeq g2) = len (FlattenSeq g1)
by POLYNOM1:31;
then A114:
dom (FlattenSeq g2) = dom (FlattenSeq g1)
by FINSEQ_3:31;
A116:
len (FlattenSeq g1) = len (prodTuples p,q,r,(FlattenSeq g2))
by A113, Def5;
X:
dom (FlattenSeq g1) = Seg (len (FlattenSeq g1))
by FINSEQ_1:def 3;
now let j be
Nat;
:: thesis: ( j in dom (FlattenSeq g1) implies (FlattenSeq g1) . j = (prodTuples p,q,r,(FlattenSeq g2)) . j )assume A117:
j in dom (FlattenSeq g1)
;
:: thesis: (FlattenSeq g1) . j = (prodTuples p,q,r,(FlattenSeq g2)) . jthen
j in dom (FlattenSeq g1)
;
then consider i1,
j1 being
Element of
NAT such that A118:
i1 in dom g1
and A119:
j1 in dom (g1 . i1)
and A120:
j = (Sum (Card (g1 | (i1 -' 1)))) + j1
and A121:
(g1 . i1) . j1 = (FlattenSeq g1) . j
by POLYNOM1:32;
A122:
i1 in Seg (len g2)
by A16, A118, FINSEQ_1:def 3;
then A123:
g1 . i1 = prodTuples p,
q,
r,
(g2 /. i1)
by A17, A18;
A124:
Seg (len (g2 /. i1)) = dom (g2 /. i1)
by FINSEQ_1:def 3;
A125:
i1 in dom g2
by A122, FINSEQ_1:def 3;
len (g1 . i1) =
len (g2 /. i1)
by A123, Def5
.=
len (g2 . i1)
by A107, A112, A118, PARTFUN1:def 8
;
then
j1 in Seg (len (g2 . i1))
by A119, FINSEQ_1:def 3;
then A126:
j1 in Seg (len (g2 /. i1))
by A125, PARTFUN1:def 8;
then A127:
j1 in dom (g2 /. i1)
by FINSEQ_1:def 3;
A128:
j in dom (FlattenSeq g2)
by A113, A117, X, FINSEQ_1:def 3;
then consider i2,
j2 being
Element of
NAT such that A129:
i2 in dom g2
and A130:
j2 in dom (g2 . i2)
and A131:
j = (Sum (Card (g2 | (i2 -' 1)))) + j2
and A132:
(g2 . i2) . j2 = (FlattenSeq g2) . j
by POLYNOM1:32;
(Sum ((Card g1) | (i1 -' 1))) + j1 =
(Sum (Card (g1 | (i1 -' 1)))) + j1
by Th16
.=
(Sum ((Card g2) | (i2 -' 1))) + j2
by A120, A131, Th16
;
then A133:
(
i1 = i2 &
j1 = j2 )
by A112, A118, A119, A129, A130, Th22;
A134:
(g2 /. i1) /. j1 =
(g2 /. i1) . j1
by A127, PARTFUN1:def 8
.=
(g2 . i1) . j1
by A125, PARTFUN1:def 8
.=
(FlattenSeq g2) /. j
by A128, A132, A133, PARTFUN1:def 8
;
thus (FlattenSeq g1) . j =
((p . (((g2 /. i1) /. j1) /. 1)) * (q . (((g2 /. i1) /. j1) /. 2))) * (r . (((g2 /. i1) /. j1) /. 3))
by A121, A123, A124, A126, Def5
.=
(prodTuples p,q,r,(FlattenSeq g2)) . j
by A114, A117, A134, Def5
;
:: thesis: verum end; then A135:
FlattenSeq g1 = prodTuples p,
q,
r,
(FlattenSeq g2)
by A116, FINSEQ_2:10;
now let y be
set ;
:: thesis: ( ( y in rng (FlattenSeq f2) implies y in rng (FlattenSeq g2) ) & ( y in rng (FlattenSeq g2) implies y in rng (FlattenSeq f2) ) )thus
(
y in rng (FlattenSeq f2) implies
y in rng (FlattenSeq g2) )
:: thesis: ( y in rng (FlattenSeq g2) implies y in rng (FlattenSeq f2) )proof
assume
y in rng (FlattenSeq f2)
;
:: thesis: y in rng (FlattenSeq g2)
then consider x being
Nat such that A136:
x in dom (FlattenSeq f2)
and A137:
(FlattenSeq f2) . x = y
by FINSEQ_2:11;
consider i1,
j1 being
Element of
NAT such that A138:
i1 in dom f2
and A139:
j1 in dom (f2 . i1)
and
x = (Sum (Card (f2 | (i1 -' 1)))) + j1
and A140:
(f2 . i1) . j1 = (FlattenSeq f2) . x
by A136, POLYNOM1:32;
A141:
i1 in Seg (i + 1)
by A7, A138, FINSEQ_1:def 3;
then A142:
f2 . i1 = (Decomp (i1 -' 1),2) ^^ (i1 |-> <*((i + 1) -' i1)*>)
by A8, A9;
then
j1 in (dom (Decomp (i1 -' 1),2)) /\ (dom (i1 |-> <*((i + 1) -' i1)*>))
by A139, MATRLIN:def 2;
then
j1 in dom (i1 |-> <*((i + 1) -' i1)*>)
by XBOOLE_0:def 4;
then A143:
j1 in Seg i1
by FUNCOP_1:19;
A144:
( 1
<= i1 &
i1 <= i + 1 )
by A141, FINSEQ_1:3;
then A145:
j1 in Seg ((i1 -' 1) + 1)
by A143, XREAL_1:237;
A146:
y =
((Decomp (i1 -' 1),2) . j1) ^ ((i1 |-> <*((i + 1) -' i1)*>) . j1)
by A137, A139, A140, A142, MATRLIN:def 2
.=
((Decomp (i1 -' 1),2) . j1) ^ <*((i + 1) -' i1)*>
by A143, FUNCOP_1:13
.=
<*(j1 -' 1),(((i1 -' 1) + 1) -' j1)*> ^ <*((i + 1) -' i1)*>
by A145, Th14
.=
<*(j1 -' 1),(i1 -' j1)*> ^ <*((i + 1) -' i1)*>
by A144, XREAL_1:237
.=
<*(j1 -' 1),(i1 -' j1),((i + 1) -' i1)*>
by FINSEQ_1:60
;
set i2 =
j1;
set j2 =
(i1 -' j1) + 1;
A147:
( 1
<= j1 &
j1 <= i1 )
by A143, FINSEQ_1:3;
then A148:
(
j1 - 1
>= 0 &
i1 - j1 >= 0 )
by XREAL_1:50;
A149:
i + 1
>= j1
by A144, A147, XXREAL_0:2;
then A150:
(i + 1) - j1 >= 0
by XREAL_1:50;
A151:
(i + 1) - i1 >= 0
by A144, XREAL_1:50;
A152:
j1 in Seg (i + 1)
by A147, A149, FINSEQ_1:3;
then A153:
j1 in dom g2
by A10, FINSEQ_1:def 3;
A154:
1
<= (i1 -' j1) + 1
by NAT_1:11;
i1 -' j1 <= (i + 1) -' j1
by A144, NAT_D:42;
then
(i1 -' j1) + 1
<= ((i + 1) -' j1) + 1
by XREAL_1:8;
then A155:
(i1 -' j1) + 1
in Seg (((i + 1) -' j1) + 1)
by A154, FINSEQ_1:3;
A156:
((i + 1) -' j1) + 1 =
((i + 1) - j1) + 1
by A150, XREAL_0:def 2
.=
(i + (1 + 1)) - j1
;
then A157:
(i1 -' j1) + 1
in Seg ((i + 2) -' j1)
by A155, XREAL_0:def 2;
A158:
g2 . j1 = (((i + 2) -' j1) |-> <*(j1 -' 1)*>) ^^ (Decomp ((i + 1) -' j1),2)
by A11, A152, A12;
A159:
dom (((i + 2) -' j1) |-> <*(j1 -' 1)*>) = Seg ((i + 2) -' j1)
by FUNCOP_1:19;
dom (Decomp ((i + 1) -' j1),2) =
Seg (len (Decomp ((i + 1) -' j1),2))
by FINSEQ_1:def 3
.=
Seg (((i + 1) -' j1) + 1)
by Th9
.=
Seg ((i + 2) -' j1)
by A156, XREAL_0:def 2
;
then
dom (g2 . j1) = (Seg ((i + 2) -' j1)) /\ (Seg ((i + 2) -' j1))
by A158, A159, MATRLIN:def 2;
then A160:
(i1 -' j1) + 1
in dom (g2 . j1)
by A155, A156, XREAL_0:def 2;
(i + 1) -' j1 >= i1 -' j1
by A144, NAT_D:42;
then
((i + 1) -' j1) + 1
>= (i1 -' j1) + 1
by XREAL_1:8;
then
(((i + 1) -' j1) + 1) - ((i1 -' j1) + 1) >= 0
by XREAL_1:50;
then A161:
(((i + 1) -' j1) + 1) -' ((i1 -' j1) + 1) =
(((i + 1) -' j1) + 1) - ((i1 -' j1) + 1)
by XREAL_0:def 2
.=
(((i + 1) -' j1) + 1) - ((i1 - j1) + 1)
by A148, XREAL_0:def 2
.=
(((i + 1) - j1) + 1) - ((1 - j1) + i1)
by A150, XREAL_0:def 2
.=
(i + 1) -' i1
by A151, XREAL_0:def 2
;
A162:
(g2 . j1) . ((i1 -' j1) + 1) =
((((i + 2) -' j1) |-> <*(j1 -' 1)*>) . ((i1 -' j1) + 1)) ^ ((Decomp ((i + 1) -' j1),2) . ((i1 -' j1) + 1))
by A158, A160, MATRLIN:def 2
.=
<*(j1 -' 1)*> ^ ((Decomp ((i + 1) -' j1),2) . ((i1 -' j1) + 1))
by A157, FUNCOP_1:13
.=
<*(j1 -' 1)*> ^ <*(((i1 -' j1) + 1) -' 1),((((i + 1) -' j1) + 1) -' ((i1 -' j1) + 1))*>
by A155, Th14
.=
<*(j1 -' 1),(((i1 -' j1) + 1) -' 1),((((i + 1) -' j1) + 1) -' ((i1 -' j1) + 1))*>
by FINSEQ_1:60
.=
<*(j1 -' 1),(i1 -' j1),((i + 1) -' i1)*>
by A161, NAT_D:34
;
(
(Sum (Card (g2 | (j1 -' 1)))) + ((i1 -' j1) + 1) in dom (FlattenSeq g2) &
(g2 . j1) . ((i1 -' j1) + 1) = (FlattenSeq g2) . ((Sum (Card (g2 | (j1 -' 1)))) + ((i1 -' j1) + 1)) )
by A153, A160, POLYNOM1:33;
hence
y in rng (FlattenSeq g2)
by A146, A162, FUNCT_1:def 5;
:: thesis: verum
end; assume
y in rng (FlattenSeq g2)
;
:: thesis: y in rng (FlattenSeq f2)then consider x being
Nat such that A163:
x in dom (FlattenSeq g2)
and A164:
(FlattenSeq g2) . x = y
by FINSEQ_2:11;
consider i1,
j1 being
Element of
NAT such that A165:
i1 in dom g2
and A166:
j1 in dom (g2 . i1)
and
x = (Sum (Card (g2 | (i1 -' 1)))) + j1
and A167:
(g2 . i1) . j1 = (FlattenSeq g2) . x
by A163, POLYNOM1:32;
A168:
i1 in Seg (i + 1)
by A10, A165, FINSEQ_1:def 3;
then A169:
g2 . i1 = (((i + 2) -' i1) |-> <*(i1 -' 1)*>) ^^ (Decomp ((i + 1) -' i1),2)
by A11, A12;
then
j1 in (dom (((i + 2) -' i1) |-> <*(i1 -' 1)*>)) /\ (dom (Decomp ((i + 1) -' i1),2))
by A166, MATRLIN:def 2;
then
j1 in dom (((i + 2) -' i1) |-> <*(i1 -' 1)*>)
by XBOOLE_0:def 4;
then A170:
j1 in Seg ((i + 2) -' i1)
by FUNCOP_1:19;
A171:
( 1
<= i1 &
i1 <= i + 1 )
by A168, FINSEQ_1:3;
then A172:
(
i1 - 1
>= 0 &
(i + 1) - i1 >= 0 )
by XREAL_1:50;
then ((i + 1) -' i1) + 1 =
((i + 1) - i1) + 1
by XREAL_0:def 2
.=
(i + (1 + 1)) - i1
;
then A173:
j1 in Seg (((i + 1) -' i1) + 1)
by A170, XREAL_0:def 2;
A174:
y =
((((i + 2) -' i1) |-> <*(i1 -' 1)*>) . j1) ^ ((Decomp ((i + 1) -' i1),2) . j1)
by A164, A166, A167, A169, MATRLIN:def 2
.=
<*(i1 -' 1)*> ^ ((Decomp ((i + 1) -' i1),2) . j1)
by A170, FUNCOP_1:13
.=
<*(i1 -' 1)*> ^ <*(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*>
by A173, Th14
.=
<*(i1 -' 1),(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*>
by FINSEQ_1:60
;
set i2 =
(j1 -' 1) + i1;
set j2 =
i1;
A175:
(j1 -' 1) + i1 >= i1
by NAT_1:11;
then A176:
(j1 -' 1) + i1 >= 1
by A171, XXREAL_0:2;
j1 >= 1
by A170, FINSEQ_1:3;
then A177:
j1 - 1
>= 0
by XREAL_1:50;
A178:
j1 <= ((i + 1) -' i1) + 1
by A173, FINSEQ_1:3;
then
j1 <= ((i + 1) - i1) + 1
by A172, XREAL_0:def 2;
then
j1 - 1
<= (i + 1) - i1
by XREAL_1:22;
then A179:
(j1 - 1) + i1 <= i + 1
by XREAL_1:21;
then
(j1 -' 1) + i1 <= i + 1
by A177, XREAL_0:def 2;
then A180:
(j1 -' 1) + i1 in Seg (i + 1)
by A176, FINSEQ_1:3;
then A181:
(j1 -' 1) + i1 in dom f2
by A7, FINSEQ_1:def 3;
A182:
i1 in Seg ((j1 -' 1) + i1)
by A171, A175, FINSEQ_1:3;
then A183:
i1 in Seg ((((j1 -' 1) + i1) -' 1) + 1)
by A171, A175, XREAL_1:237, XXREAL_0:2;
A184:
f2 . ((j1 -' 1) + i1) = (Decomp (((j1 -' 1) + i1) -' 1),2) ^^ (((j1 -' 1) + i1) |-> <*((i + 1) -' ((j1 -' 1) + i1))*>)
by A8, A180, A9;
A185:
dom (((j1 -' 1) + i1) |-> <*((i + 1) -' ((j1 -' 1) + i1))*>) = Seg ((j1 -' 1) + i1)
by FUNCOP_1:19;
dom (Decomp (((j1 -' 1) + i1) -' 1),2) =
Seg (len (Decomp (((j1 -' 1) + i1) -' 1),2))
by FINSEQ_1:def 3
.=
Seg ((((j1 -' 1) + i1) -' 1) + 1)
by Th9
.=
Seg ((j1 -' 1) + i1)
by A171, A175, XREAL_1:237, XXREAL_0:2
;
then
dom (f2 . ((j1 -' 1) + i1)) = (Seg ((j1 -' 1) + i1)) /\ (Seg ((j1 -' 1) + i1))
by A184, A185, MATRLIN:def 2;
then A186:
i1 in dom (f2 . ((j1 -' 1) + i1))
by A171, A175, FINSEQ_1:3;
A187:
(((i + 1) -' i1) + 1) - j1 >= 0
by A178, XREAL_1:50;
(i + 1) - ((j1 - 1) + i1) >= 0
by A179, XREAL_1:50;
then
(i + 1) - ((j1 -' 1) + i1) >= 0
by A177, XREAL_0:def 2;
then A188:
(i + 1) -' ((j1 -' 1) + i1) =
(i + 1) - ((j1 -' 1) + i1)
by XREAL_0:def 2
.=
(i + 1) - ((j1 - 1) + i1)
by A177, XREAL_0:def 2
.=
(((i + 1) - i1) + 1) - j1
.=
(((i + 1) -' i1) + 1) - j1
by A172, XREAL_0:def 2
.=
(((i + 1) -' i1) + 1) -' j1
by A187, XREAL_0:def 2
;
A189:
(f2 . ((j1 -' 1) + i1)) . i1 =
((Decomp (((j1 -' 1) + i1) -' 1),2) . i1) ^ ((((j1 -' 1) + i1) |-> <*((i + 1) -' ((j1 -' 1) + i1))*>) . i1)
by A184, A186, MATRLIN:def 2
.=
((Decomp (((j1 -' 1) + i1) -' 1),2) . i1) ^ <*((i + 1) -' ((j1 -' 1) + i1))*>
by A182, FUNCOP_1:13
.=
<*(i1 -' 1),(((((j1 -' 1) + i1) -' 1) + 1) -' i1)*> ^ <*((i + 1) -' ((j1 -' 1) + i1))*>
by A183, Th14
.=
<*(i1 -' 1),(((((j1 -' 1) + i1) -' 1) + 1) -' i1),((i + 1) -' ((j1 -' 1) + i1))*>
by FINSEQ_1:60
.=
<*(i1 -' 1),(((j1 -' 1) + i1) -' i1),((i + 1) -' ((j1 -' 1) + i1))*>
by A171, A175, XREAL_1:237, XXREAL_0:2
.=
<*(i1 -' 1),(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*>
by A188, NAT_D:34
;
(
(Sum (Card (f2 | (((j1 -' 1) + i1) -' 1)))) + i1 in dom (FlattenSeq f2) &
(f2 . ((j1 -' 1) + i1)) . i1 = (FlattenSeq f2) . ((Sum (Card (f2 | (((j1 -' 1) + i1) -' 1)))) + i1) )
by A181, A186, POLYNOM1:33;
hence
y in rng (FlattenSeq f2)
by A174, A189, FUNCT_1:def 5;
:: thesis: verum end; then A190:
rng (FlattenSeq f2) = rng (FlattenSeq g2)
by TARSKI:2;
A191:
dom (Card f2) =
dom f2
by CARD_3:def 2
.=
Seg (len g2)
by A7, A10, FINSEQ_1:def 3
.=
dom g2
by FINSEQ_1:def 3
.=
dom (Card g2)
by CARD_3:def 2
.=
dom (Rev (Card g2))
by FINSEQ_5:60
;
then A192:
len (Card f2) = len (Rev (Card g2))
by FINSEQ_3:31;
now let j be
Nat;
:: thesis: ( j in dom (Card f2) implies (Card f2) . j = (Rev (Card g2)) . j )assume
j in dom (Card f2)
;
:: thesis: (Card f2) . j = (Rev (Card g2)) . jthen A193:
j in dom (Card f2)
;
then A194:
j in dom f2
by CARD_3:def 2;
A195:
dom (Card g2) = dom g2
by CARD_3:def 2;
then A196:
len (Card g2) = len g2
by FINSEQ_3:31;
A197:
j in Seg (len (Rev (Card g2)))
by A191, A193, FINSEQ_1:def 3;
then A198:
j in Seg (len g2)
by A196, FINSEQ_5:def 3;
then
((len (Card g2)) - j) + 1
in Seg (len g2)
by A196, FINSEQ_5:2;
then A199:
((len (Card g2)) - j) + 1
in dom g2
by FINSEQ_1:def 3;
A200:
j >= 1
by A197, FINSEQ_1:3;
A201:
i + 1
>= j
by A10, A198, FINSEQ_1:3;
A202:
f2 . j = (Decomp (j -' 1),2) ^^ (j |-> <*((i + 1) -' j)*>)
by A8, A10, A198, A9;
A203:
dom (Decomp (j -' 1),2) =
Seg (len (Decomp (j -' 1),2))
by FINSEQ_1:def 3
.=
Seg ((j -' 1) + 1)
by Th9
.=
Seg j
by A200, XREAL_1:237
;
A204:
dom (j |-> <*((i + 1) -' j)*>) = Seg j
by FUNCOP_1:19;
Seg (len (f2 . j)) =
dom (f2 . j)
by FINSEQ_1:def 3
.=
(Seg j) /\ (Seg j)
by A202, A203, A204, MATRLIN:def 2
.=
Seg j
;
then A205:
len (f2 . j) = j
by FINSEQ_1:8;
A206:
(i + 1) - j >= 0
by A201, XREAL_1:50;
then
((i + 1) - j) + 1
= ((i + 1) -' j) + 1
by XREAL_0:def 2;
then reconsider lj =
((len (Card g2)) - j) + 1 as
Element of
NAT by A10, A195, FINSEQ_3:31;
(i + 1) - (((i + 1) - j) + 1) = 0 + (j - 1)
;
then A207:
(i + 1) - (((i + 1) - j) + 1) >= 0
by A200, XREAL_1:50;
then A208:
((i + 1) -' lj) + 1 =
(0 + (j - 1)) + 1
by A10, A196, XREAL_0:def 2
.=
j
;
A209:
((i + 1) - j) + 1
>= 0 + 1
by A206, XREAL_1:8;
j - 1
>= 0
by A200, XREAL_1:50;
then
(i + 1) - (j - 1) <= i + 1
by XREAL_1:45;
then
lj in Seg (i + 1)
by A10, A196, A209, FINSEQ_1:3;
then A210:
g2 . lj = (((i + 2) -' lj) |-> <*(lj -' 1)*>) ^^ (Decomp ((i + 1) -' lj),2)
by A11, A12;
A211:
dom (Decomp ((i + 1) -' lj),2) =
Seg (len (Decomp ((i + 1) -' lj),2))
by FINSEQ_1:def 3
.=
Seg j
by A208, Th9
;
A212:
((i + 1) -' lj) + 1 =
((i + 1) - lj) + 1
by A10, A196, A207, XREAL_0:def 2
.=
(i + (1 + 1)) - lj
;
A213:
dom (((i + 2) -' lj) |-> <*(lj -' 1)*>) =
Seg ((i + 2) -' lj)
by FUNCOP_1:19
.=
Seg j
by A208, A212, XREAL_0:def 2
;
Seg (len (g2 . lj)) =
dom (g2 . lj)
by FINSEQ_1:def 3
.=
(Seg j) /\ (Seg j)
by A210, A211, A213, MATRLIN:def 2
.=
Seg j
;
then A214:
len (g2 . lj) = j
by FINSEQ_1:8;
thus (Card f2) . j =
j
by A194, A205, CARD_3:def 2
.=
(Card g2) . (((len (Card g2)) - j) + 1)
by A199, A214, CARD_3:def 2
.=
(Rev (Card g2)) . j
by A191, A193, FINSEQ_5:def 3
;
:: thesis: verum end; then A215:
Card f2 = Rev (Card g2)
by A192, FINSEQ_2:10;
reconsider w =
Card g2 as
FinSequence of
NAT ;
A216:
len (FlattenSeq f2) =
Sum (Card f2)
by POLYNOM1:30
.=
Sum w
by A215, Th3
.=
len (FlattenSeq g2)
by POLYNOM1:30
;
now let x,
y be
set ;
:: thesis: ( x in dom (FlattenSeq g2) & y in dom (FlattenSeq g2) & (FlattenSeq g2) . x = (FlattenSeq g2) . y implies x = y )assume that A217:
x in dom (FlattenSeq g2)
and A218:
y in dom (FlattenSeq g2)
and A219:
(FlattenSeq g2) . x = (FlattenSeq g2) . y
;
:: thesis: x = yconsider i1,
j1 being
Element of
NAT such that A220:
i1 in dom g2
and A221:
j1 in dom (g2 . i1)
and A222:
x = (Sum (Card (g2 | (i1 -' 1)))) + j1
and A223:
(g2 . i1) . j1 = (FlattenSeq g2) . x
by A217, POLYNOM1:32;
consider i2,
j2 being
Element of
NAT such that A224:
i2 in dom g2
and A225:
j2 in dom (g2 . i2)
and A226:
y = (Sum (Card (g2 | (i2 -' 1)))) + j2
and A227:
(g2 . i2) . j2 = (FlattenSeq g2) . y
by A218, POLYNOM1:32;
A228:
i1 in Seg (i + 1)
by A10, A220, FINSEQ_1:def 3;
then A229:
g2 . i1 = (((i + 2) -' i1) |-> <*(i1 -' 1)*>) ^^ (Decomp ((i + 1) -' i1),2)
by A11, A12;
A230:
i2 in Seg (i + 1)
by A10, A224, FINSEQ_1:def 3;
then A231:
g2 . i2 = (((i + 2) -' i2) |-> <*(i2 -' 1)*>) ^^ (Decomp ((i + 1) -' i2),2)
by A11, A12;
(
j1 in Seg (len (g2 . i1)) &
j2 in Seg (len (g2 . i2)) )
by A221, A225, FINSEQ_1:def 3;
then A232:
(
i1 >= 1 &
i2 >= 1 &
j1 >= 1 &
j2 >= 1 )
by A228, A230, FINSEQ_1:3;
A233:
i1 <= i + 1
by A228, FINSEQ_1:3;
then A234:
(i + 1) - i1 >= 0
by XREAL_1:50;
A235:
(i + 1) + 1
>= i + 1
by NAT_1:11;
then
(i + 1) + 1
>= i1
by A233, XXREAL_0:2;
then A236:
(i + 2) - i1 >= 0
by XREAL_1:50;
A237:
((i + 1) -' i1) + 1 =
((i + 1) - i1) + 1
by A234, XREAL_0:def 2
.=
(i + 2) -' i1
by A236, XREAL_0:def 2
;
A238:
dom (((i + 2) -' i1) |-> <*(i1 -' 1)*>) = Seg ((i + 2) -' i1)
by FUNCOP_1:19;
dom (Decomp ((i + 1) -' i1),2) =
Seg (len (Decomp ((i + 1) -' i1),2))
by FINSEQ_1:def 3
.=
Seg ((i + 2) -' i1)
by A237, Th9
;
then A239:
dom (g2 . i1) =
(Seg ((i + 2) -' i1)) /\ (Seg ((i + 2) -' i1))
by A229, A238, MATRLIN:def 2
.=
Seg ((i + 2) -' i1)
;
A240:
i2 <= i + 1
by A230, FINSEQ_1:3;
then A241:
(i + 1) - i2 >= 0
by XREAL_1:50;
(i + 1) + 1
>= i2
by A235, A240, XXREAL_0:2;
then A242:
(i + 2) - i2 >= 0
by XREAL_1:50;
A243:
((i + 1) -' i2) + 1 =
((i + 1) - i2) + 1
by A241, XREAL_0:def 2
.=
(i + 2) -' i2
by A242, XREAL_0:def 2
;
A244:
dom (((i + 2) -' i2) |-> <*(i2 -' 1)*>) = Seg ((i + 2) -' i2)
by FUNCOP_1:19;
dom (Decomp ((i + 1) -' i2),2) =
Seg (len (Decomp ((i + 1) -' i2),2))
by FINSEQ_1:def 3
.=
Seg ((i + 2) -' i2)
by A243, Th9
;
then A245:
dom (g2 . i2) =
(Seg ((i + 2) -' i2)) /\ (Seg ((i + 2) -' i2))
by A231, A244, MATRLIN:def 2
.=
Seg ((i + 2) -' i2)
;
A246:
(g2 . i1) . j1 =
((((i + 2) -' i1) |-> <*(i1 -' 1)*>) . j1) ^ ((Decomp ((i + 1) -' i1),2) . j1)
by A221, A229, MATRLIN:def 2
.=
<*(i1 -' 1)*> ^ ((Decomp ((i + 1) -' i1),2) . j1)
by A221, A239, FUNCOP_1:13
.=
<*(i1 -' 1)*> ^ <*(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*>
by A221, A237, A239, Th14
.=
<*(i1 -' 1),(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*>
by FINSEQ_1:60
;
(g2 . i2) . j2 =
((((i + 2) -' i2) |-> <*(i2 -' 1)*>) . j2) ^ ((Decomp ((i + 1) -' i2),2) . j2)
by A225, A231, MATRLIN:def 2
.=
<*(i2 -' 1)*> ^ ((Decomp ((i + 1) -' i2),2) . j2)
by A225, A245, FUNCOP_1:13
.=
<*(i2 -' 1)*> ^ <*(j2 -' 1),((((i + 1) -' i2) + 1) -' j2)*>
by A225, A243, A245, Th14
.=
<*(i2 -' 1),(j2 -' 1),((((i + 1) -' i2) + 1) -' j2)*>
by FINSEQ_1:60
;
then
(
i1 -' 1
= i2 -' 1 &
j1 -' 1
= j2 -' 1 )
by A219, A223, A227, A246, GROUP_7:3;
hence
x = y
by A222, A226, A232, XREAL_1:236;
:: thesis: verum end; then A247:
FlattenSeq g2 is
one-to-one
by FUNCT_1:def 8;
then
FlattenSeq f2 is
one-to-one
by A190, A216, FINSEQ_4:76;
then
FlattenSeq f2,
FlattenSeq g2 are_fiberwise_equipotent
by A190, A247, RFINSEQ:39;
then consider P being
Permutation of
(dom (FlattenSeq g2)) such that A248:
FlattenSeq f2 = (FlattenSeq g2) * P
by RFINSEQ:17;
reconsider P =
P as
Permutation of
(dom (FlattenSeq g1)) by A114;
FlattenSeq f1 = (FlattenSeq g1) * P
by A106, A135, A248, Th15;
hence
((p *' q) *' r) . i = (p *' (q *' r)) . i
by A2, A5, A47, A78, RLVECT_2:9;
:: thesis: verum end;
hence
(p *' q) *' r = p *' (q *' r)
by FUNCT_2:113; :: thesis: verum