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