let L be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 for i being Element of NAT holds ((p *' q) *' r) . i = (p *' (q *' r)) . ilet 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 Def9;
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 for j being Nat st j in dom (Card f2) holds
(Card f2) . j = (Rev (Card g2)) . jlet 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 for y being object holds
( ( y in rng (FlattenSeq f2) implies y in rng (FlattenSeq g2) ) & ( y in rng (FlattenSeq g2) implies y in rng (FlattenSeq f2) ) )let y be
object ;
( ( 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
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
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:2;
now for x, y being object st x in dom (FlattenSeq g2) & y in dom (FlattenSeq g2) & (FlattenSeq g2) . x = (FlattenSeq g2) . y holds
x = yA88:
(i + 1) + 1
>= i + 1
by NAT_1:11;
let x,
y be
object ;
( 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
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
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;
A116:
w is
FinSequence of
REAL
by FINSEQ_2:24, NUMBERS:19;
len (FlattenSeq f2) =
Sum (Card f2)
by PRE_POLY:27
.=
Sum w
by A33, Th3, A116
.=
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 A117:
FlattenSeq f2 = (FlattenSeq g2) * P
by RFINSEQ:4;
A118:
dom (Card g2) = dom g2
by CARD_3:def 2;
then A119:
len (Card g2) = len g2
by FINSEQ_3:29;
consider r1 being
FinSequence of the
carrier of
L such that A120:
len r1 = i + 1
and A121:
((p *' q) *' r) . i = Sum r1
and A122:
for
k being
Element of
NAT st
k in dom r1 holds
r1 . k = ((p *' q) . (k -' 1)) * (r . ((i + 1) -' k))
by Def9;
A123:
dom r1 = Seg (i + 1)
by A120, 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 A124:
len f1 = len f2
and A125:
for
k being
Nat st
k in dom f1 holds
f1 . k = H3(
k)
from FINSEQ_2:sch 1();
A126:
dom f1 = Seg (len f2)
by A124, FINSEQ_1:def 3;
A127:
now for j being Nat st j in dom r1 holds
r1 . j = (Sum f1) . jlet j be
Nat;
( j in dom r1 implies r1 . j = (Sum f1) . j )A128:
dom (j |-> <*((i + 1) -' j)*>) = Seg j
by FUNCOP_1:13;
consider r3 being
FinSequence of the
carrier of
L such that A129:
len r3 = (j -' 1) + 1
and A130:
(p *' q) . (j -' 1) = Sum r3
and A131:
for
k being
Element of
NAT st
k in dom r3 holds
r3 . k = (p . (k -' 1)) * (q . (((j -' 1) + 1) -' k))
by Def9;
assume A132:
j in dom r1
;
r1 . j = (Sum f1) . jthen A133:
1
<= j
by A123, FINSEQ_1:1;
then A134:
len r3 = j
by A129, XREAL_1:235;
len (Decomp ((j -' 1),2)) =
(j -' 1) + 1
by Th9
.=
j
by A133, XREAL_1:235
;
then A135:
dom (Decomp ((j -' 1),2)) = Seg j
by FINSEQ_1:def 3;
A136:
dom r1 = dom f1
by A120, A1, A124, FINSEQ_3:29;
then A137:
f1 /. j =
f1 . j
by A132, PARTFUN1:def 6
.=
prodTuples (
p,
q,
r,
(f2 /. j))
by A1, A125, A126, A123, A132
;
dom f1 = dom f2
by A124, FINSEQ_3:29;
then A138:
f2 /. j =
f2 . j
by A132, A136, PARTFUN1:def 6
.=
(Decomp ((j -' 1),2)) ^^ (j |-> <*((i + 1) -' j)*>)
by A2, A3, A123, A132
;
then A139:
dom (f2 /. j) =
(dom (Decomp ((j -' 1),2))) /\ (dom (j |-> <*((i + 1) -' j)*>))
by PRE_POLY:def 4
.=
Seg j
by A135, A128
;
A140:
len (prodTuples (p,q,r,(f2 /. j))) =
len (f2 /. j)
by Def5
.=
j
by A132, A139, FINSEQ_1:def 3
;
then A141:
dom (prodTuples (p,q,r,(f2 /. j))) = Seg j
by FINSEQ_1:def 3;
A142:
dom (r3 * (r . ((i + 1) -' j))) = dom r3
by POLYNOM1:def 2;
A143:
now for k being Nat st k in dom (prodTuples (p,q,r,(f2 /. j))) holds
(prodTuples (p,q,r,(f2 /. j))) . k = (r3 * (r . ((i + 1) -' j))) . klet 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 A144:
k in dom (prodTuples (p,q,r,(f2 /. j)))
;
(prodTuples (p,q,r,(f2 /. j))) . k = (r3 * (r . ((i + 1) -' j))) . kthen A145:
(f2 /. j) /. k =
(f2 /. j) . k
by A139, A141, PARTFUN1:def 6
.=
((Decomp ((j -' 1),2)) . k) ^ ((j |-> <*((i + 1) -' j)*>) . k)
by A138, A139, A141, A144, PRE_POLY:def 4
.=
<*(k -' 1),(((j -' 1) + 1) -' k)*> ^ ((j |-> <*((i + 1) -' j)*>) . k)
by A129, A134, A141, A144, Th14
.=
<*(k -' 1),(((j -' 1) + 1) -' k)*> ^ <*((i + 1) -' j)*>
by A141, A144, 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 A145, FINSEQ_1:45;
then
1
in dom ((f2 /. j) /. k)
by FINSEQ_1:def 3;
then A146:
((f2 /. j) /. k) /. 1 =
((f2 /. j) /. k) . 1
by PARTFUN1:def 6
.=
k -' 1
by A145, FINSEQ_1:45
;
A147:
k in dom r3
by A134, A141, A144, FINSEQ_1:def 3;
then A148:
r3 /. k =
r3 . k
by PARTFUN1:def 6
.=
(p . (k -' 1)) * (q . (((j -' 1) + 1) -' k))
by A131, A147
;
3
in Seg 3
by ENUMSET1:def 1, FINSEQ_3:1;
then
3
in Seg (len ((f2 /. j) /. k))
by A145, FINSEQ_1:45;
then
3
in dom ((f2 /. j) /. k)
by FINSEQ_1:def 3;
then A149:
((f2 /. j) /. k) /. 3 =
((f2 /. j) /. k) . 3
by PARTFUN1:def 6
.=
(i + 1) -' j
by A145, FINSEQ_1:45
;
2
in Seg 3
by ENUMSET1:def 1, FINSEQ_3:1;
then
2
in Seg (len ((f2 /. j) /. k))
by A145, FINSEQ_1:45;
then
2
in dom ((f2 /. j) /. k)
by FINSEQ_1:def 3;
then A150:
((f2 /. j) /. k) /. 2 =
((f2 /. j) /. k) . 2
by PARTFUN1:def 6
.=
((j -' 1) + 1) -' k
by A145, 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 A139, A141, A144, Def5
.=
(r3 * (r . ((i + 1) -' j))) /. k
by A147, A148, A146, A150, A149, POLYNOM1:def 2
.=
(r3 * (r . ((i + 1) -' j))) . k
by A142, A147, PARTFUN1:def 6
;
verum end;
len f1 = len (Sum f1)
by MATRLIN:def 6;
then A151:
dom f1 = dom (Sum f1)
by FINSEQ_3:29;
len (r3 * (r . ((i + 1) -' j))) = len r3
by A142, FINSEQ_3:29;
then A152:
prodTuples (
p,
q,
r,
(f2 /. j))
= r3 * (r . ((i + 1) -' j))
by A140, A134, A143, FINSEQ_2:9;
((p *' q) . (j -' 1)) * (r . ((i + 1) -' j)) = Sum (r3 * (r . ((i + 1) -' j)))
by A130, POLYNOM1:13;
hence r1 . j =
Sum (r3 * (r . ((i + 1) -' j)))
by A122, A132
.=
(Sum f1) /. j
by A132, A151, A136, A137, A152, MATRLIN:def 6
.=
(Sum f1) . j
by A132, A151, A136, 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 A153:
len g1 = len g2
and A154:
for
k being
Nat st
k in dom g1 holds
g1 . k = H4(
k)
from FINSEQ_2:sch 1();
A155:
dom g1 = Seg (len g2)
by A153, FINSEQ_1:def 3;
A156:
now for j being Nat st j in dom r2 holds
r2 . j = (Sum g1) . jlet j be
Nat;
( j in dom r2 implies r2 . j = (Sum g1) . j )A157:
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 A158:
len r3 = ((i + 1) -' j) + 1
and A159:
(q *' r) . ((i + 1) -' j) = Sum r3
and A160:
for
k being
Element of
NAT st
k in dom r3 holds
r3 . k = (q . (k -' 1)) * (r . ((((i + 1) -' j) + 1) -' k))
by Def9;
assume A161:
j in dom r2
;
r2 . j = (Sum g1) . jthen A162:
j <= i + 1
by A10, FINSEQ_1:1;
(i + 1) + 1
>= i + 1
by NAT_1:11;
then
(i + 1) + 1
>= j
by A162, XXREAL_0:2;
then A163:
(i + 2) - j >= 0
by XREAL_1:48;
(i + 1) - j >= 0
by A162, XREAL_1:48;
then A164:
((i + 1) -' j) + 1 =
((i + 1) - j) + 1
by XREAL_0:def 2
.=
(i + 2) -' j
by A163, XREAL_0:def 2
;
then
len (Decomp (((i + 1) -' j),2)) = (i + 2) -' j
by Th9;
then A165:
dom (Decomp (((i + 1) -' j),2)) = Seg ((i + 2) -' j)
by FINSEQ_1:def 3;
A166:
dom r2 = dom g1
by A7, A4, A153, FINSEQ_3:29;
then A167:
g1 /. j =
g1 . j
by A161, PARTFUN1:def 6
.=
prodTuples (
p,
q,
r,
(g2 /. j))
by A4, A154, A155, A10, A161
;
dom g1 = dom g2
by A153, FINSEQ_3:29;
then A168:
g2 /. j =
g2 . j
by A161, A166, PARTFUN1:def 6
.=
(((i + 2) -' j) |-> <*(j -' 1)*>) ^^ (Decomp (((i + 1) -' j),2))
by A5, A6, A10, A161
;
then A169:
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 A165, A157
;
A170:
len (prodTuples (p,q,r,(g2 /. j))) =
len (g2 /. j)
by Def5
.=
(i + 2) -' j
by A169, FINSEQ_1:def 3
;
then A171:
dom (prodTuples (p,q,r,(g2 /. j))) = Seg ((i + 2) -' j)
by FINSEQ_1:def 3;
A172:
dom ((p . (j -' 1)) * r3) = dom r3
by POLYNOM1:def 1;
A173:
now for k being Nat st k in dom (prodTuples (p,q,r,(g2 /. j))) holds
(prodTuples (p,q,r,(g2 /. j))) . k = ((p . (j -' 1)) * r3) . klet 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 A174:
k in dom (prodTuples (p,q,r,(g2 /. j)))
;
(prodTuples (p,q,r,(g2 /. j))) . k = ((p . (j -' 1)) * r3) . kthen A175:
(g2 /. j) /. k =
(g2 /. j) . k
by A169, A171, PARTFUN1:def 6
.=
((((i + 2) -' j) |-> <*(j -' 1)*>) . k) ^ ((Decomp (((i + 1) -' j),2)) . k)
by A168, A169, A171, A174, PRE_POLY:def 4
.=
((((i + 2) -' j) |-> <*(j -' 1)*>) . k) ^ <*(k -' 1),((((i + 1) -' j) + 1) -' k)*>
by A164, A171, A174, Th14
.=
<*(j -' 1)*> ^ <*(k -' 1),((((i + 1) -' j) + 1) -' k)*>
by A171, A174, 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 A175, FINSEQ_1:45;
then
1
in dom ((g2 /. j) /. k)
by FINSEQ_1:def 3;
then A176:
((g2 /. j) /. k) /. 1 =
((g2 /. j) /. k) . 1
by PARTFUN1:def 6
.=
j -' 1
by A175, FINSEQ_1:45
;
A177:
k in dom r3
by A158, A164, A171, A174, FINSEQ_1:def 3;
then A178:
r3 /. k =
r3 . k
by PARTFUN1:def 6
.=
(q . (k -' 1)) * (r . ((((i + 1) -' j) + 1) -' k))
by A160, A177
;
3
in Seg 3
by ENUMSET1:def 1, FINSEQ_3:1;
then
3
in Seg (len ((g2 /. j) /. k))
by A175, FINSEQ_1:45;
then
3
in dom ((g2 /. j) /. k)
by FINSEQ_1:def 3;
then A179:
((g2 /. j) /. k) /. 3 =
((g2 /. j) /. k) . 3
by PARTFUN1:def 6
.=
(((i + 1) -' j) + 1) -' k
by A175, FINSEQ_1:45
;
2
in Seg 3
by ENUMSET1:def 1, FINSEQ_3:1;
then
2
in Seg (len ((g2 /. j) /. k))
by A175, FINSEQ_1:45;
then
2
in dom ((g2 /. j) /. k)
by FINSEQ_1:def 3;
then A180:
((g2 /. j) /. k) /. 2 =
((g2 /. j) /. k) . 2
by PARTFUN1:def 6
.=
k -' 1
by A175, 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 A169, A171, A174, 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 A177, A178, A176, A180, A179, POLYNOM1:def 1
.=
((p . (j -' 1)) * r3) . k
by A172, A177, PARTFUN1:def 6
;
verum end;
len g1 = len (Sum g1)
by MATRLIN:def 6;
then A181:
dom g1 = dom (Sum g1)
by FINSEQ_3:29;
len ((p . (j -' 1)) * r3) = len r3
by A172, FINSEQ_3:29;
then A182:
prodTuples (
p,
q,
r,
(g2 /. j))
= (p . (j -' 1)) * r3
by A158, A164, A170, A173, FINSEQ_2:9;
(p . (j -' 1)) * ((q *' r) . ((i + 1) -' j)) = Sum ((p . (j -' 1)) * r3)
by A159, POLYNOM1:12;
hence r2 . j =
Sum ((p . (j -' 1)) * r3)
by A9, A161
.=
(Sum g1) /. j
by A161, A181, A166, A167, A182, MATRLIN:def 6
.=
(Sum g1) . j
by A161, A181, A166, PARTFUN1:def 6
;
verum end; A183:
dom (Card g2) = Seg (i + 1)
by A4, A118, FINSEQ_1:def 3;
A184:
now for j being Nat st j in dom (Card g2) holds
(Card g2) . j = (Card g1) . jlet j be
Nat;
( j in dom (Card g2) implies (Card g2) . j = (Card g1) . j )assume A185:
j in dom (Card g2)
;
(Card g2) . j = (Card g1) . jthen A186:
j in dom g1
by A4, A153, A183, FINSEQ_1:def 3;
g1 . j = prodTuples (
p,
q,
r,
(g2 /. j))
by A4, A154, A155, A183, A185;
then A187:
len (g1 . j) =
len (g2 /. j)
by Def5
.=
len (g2 . j)
by A118, A185, PARTFUN1:def 6
;
thus (Card g2) . j =
len (g2 . j)
by A118, A185, CARD_3:def 2
.=
(Card g1) . j
by A186, A187, CARD_3:def 2
;
verum end; A188:
dom (Card g1) = dom g1
by CARD_3:def 2;
then
len (Card g1) = len g1
by FINSEQ_3:29;
then A189:
Card g2 = Card g1
by A153, A119, A184, FINSEQ_2:9;
then A190:
len (FlattenSeq g2) = len (FlattenSeq g1)
by PRE_POLY:28;
then A191:
dom (FlattenSeq g2) = dom (FlattenSeq g1)
by FINSEQ_3:29;
then reconsider P =
P as
Permutation of
(dom (FlattenSeq g1)) ;
A192:
dom (FlattenSeq g1) = Seg (len (FlattenSeq g1))
by FINSEQ_1:def 3;
A193:
now for j being Nat st j in dom (FlattenSeq g1) holds
(FlattenSeq g1) . j = (prodTuples (p,q,r,(FlattenSeq g2))) . jlet j be
Nat;
( j in dom (FlattenSeq g1) implies (FlattenSeq g1) . j = (prodTuples (p,q,r,(FlattenSeq g2))) . j )assume A194:
j in dom (FlattenSeq g1)
;
(FlattenSeq g1) . j = (prodTuples (p,q,r,(FlattenSeq g2))) . jthen consider i1,
j1 being
Nat such that A195:
i1 in dom g1
and A196:
j1 in dom (g1 . i1)
and A197:
j = (Sum (Card (g1 | (i1 -' 1)))) + j1
and A198:
(g1 . i1) . j1 = (FlattenSeq g1) . j
by PRE_POLY:29;
A199:
j in dom (FlattenSeq g2)
by A190, A192, A194, FINSEQ_1:def 3;
then consider i2,
j2 being
Nat such that A200:
(
i2 in dom g2 &
j2 in dom (g2 . i2) )
and A201:
j = (Sum (Card (g2 | (i2 -' 1)))) + j2
and A202:
(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 A197, A201, Th16
;
then A203:
(
i1 = i2 &
j1 = j2 )
by A189, A195, A196, A200, Th21;
i1 in Seg (len g2)
by A153, A195, FINSEQ_1:def 3;
then A204:
i1 in dom g2
by FINSEQ_1:def 3;
A205:
g1 . i1 = prodTuples (
p,
q,
r,
(g2 /. i1))
by A154, A195;
then len (g1 . i1) =
len (g2 /. i1)
by Def5
.=
len (g2 . i1)
by A188, A118, A189, A195, PARTFUN1:def 6
;
then
j1 in Seg (len (g2 . i1))
by A196, FINSEQ_1:def 3;
then A206:
j1 in Seg (len (g2 /. i1))
by A204, PARTFUN1:def 6;
then
j1 in dom (g2 /. i1)
by FINSEQ_1:def 3;
then A207:
(g2 /. i1) /. j1 =
(g2 /. i1) . j1
by PARTFUN1:def 6
.=
(g2 . i1) . j1
by A204, PARTFUN1:def 6
.=
(FlattenSeq g2) /. j
by A199, A202, A203, 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 A198, A205, A206, Def5
.=
(prodTuples (p,q,r,(FlattenSeq g2))) . j
by A191, A194, A207, Def5
;
verum end; A208:
dom (Card f2) = dom f2
by CARD_3:def 2;
then A209:
len (Card f2) = len f2
by FINSEQ_3:29;
A210:
dom (Card f2) = Seg (i + 1)
by A1, A208, FINSEQ_1:def 3;
A211:
now for j being Nat st j in dom (Card f2) holds
(Card f2) . j = (Card f1) . jlet j be
Nat;
( j in dom (Card f2) implies (Card f2) . j = (Card f1) . j )assume A212:
j in dom (Card f2)
;
(Card f2) . j = (Card f1) . jthen A213:
j in dom f1
by A1, A124, A210, FINSEQ_1:def 3;
f1 . j = prodTuples (
p,
q,
r,
(f2 /. j))
by A1, A125, A126, A210, A212;
then A214:
len (f1 . j) =
len (f2 /. j)
by Def5
.=
len (f2 . j)
by A208, A212, PARTFUN1:def 6
;
thus (Card f2) . j =
len (f2 . j)
by A208, A212, CARD_3:def 2
.=
(Card f1) . j
by A213, A214, CARD_3:def 2
;
verum end; A215:
dom (Card f1) = dom f1
by CARD_3:def 2;
then
len (Card f1) = len f1
by FINSEQ_3:29;
then A216:
Card f2 = Card f1
by A124, A209, A211, FINSEQ_2:9;
then A217:
len (FlattenSeq f1) = len (FlattenSeq f2)
by PRE_POLY:28;
A218:
Seg (len (FlattenSeq f1)) = dom (FlattenSeq f1)
by FINSEQ_1:def 3;
A219:
now for j being Nat st j in dom (FlattenSeq f1) holds
(FlattenSeq f1) . j = (prodTuples (p,q,r,(FlattenSeq f2))) . jlet j be
Nat;
( j in dom (FlattenSeq f1) implies (FlattenSeq f1) . j = (prodTuples (p,q,r,(FlattenSeq f2))) . j )assume A220:
j in dom (FlattenSeq f1)
;
(FlattenSeq f1) . j = (prodTuples (p,q,r,(FlattenSeq f2))) . jthen consider i1,
j1 being
Nat such that A221:
i1 in dom f1
and A222:
j1 in dom (f1 . i1)
and A223:
j = (Sum (Card (f1 | (i1 -' 1)))) + j1
and A224:
(f1 . i1) . j1 = (FlattenSeq f1) . j
by PRE_POLY:29;
A225:
j in dom (FlattenSeq f2)
by A217, A34, A220, FINSEQ_1:def 3;
then consider i2,
j2 being
Nat such that A226:
(
i2 in dom f2 &
j2 in dom (f2 . i2) )
and A227:
j = (Sum (Card (f2 | (i2 -' 1)))) + j2
and A228:
(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 A223, A227, Th16
;
then A229:
(
i1 = i2 &
j1 = j2 )
by A216, A221, A222, A226, Th21;
i1 in Seg (len f2)
by A124, A221, FINSEQ_1:def 3;
then A230:
i1 in dom f2
by FINSEQ_1:def 3;
A231:
f1 . i1 = prodTuples (
p,
q,
r,
(f2 /. i1))
by A125, A221;
then len (f1 . i1) =
len (f2 /. i1)
by Def5
.=
len (f2 . i1)
by A215, A208, A216, A221, PARTFUN1:def 6
;
then
j1 in Seg (len (f2 . i1))
by A222, FINSEQ_1:def 3;
then A232:
j1 in Seg (len (f2 /. i1))
by A230, PARTFUN1:def 6;
then
j1 in dom (f2 /. i1)
by FINSEQ_1:def 3;
then A233:
(f2 /. i1) /. j1 =
(f2 /. i1) . j1
by PARTFUN1:def 6
.=
(f2 . i1) . j1
by A230, PARTFUN1:def 6
.=
(FlattenSeq f2) /. j
by A225, A228, A229, 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 A224, A231, A232, Def5
.=
((p . (((FlattenSeq f2) /. j) /. 1)) * (q . (((FlattenSeq f2) /. j) /. 2))) * (r . (((FlattenSeq f2) /. j) /. 3))
by A233
.=
(prodTuples (p,q,r,(FlattenSeq f2))) . j
by A217, A34, A218, A220, Def5
;
verum end;
len (Sum g1) = i + 1
by A4, A153, MATRLIN:def 6;
then
r2 = Sum g1
by A7, A156, FINSEQ_2:9;
then A234:
Sum r2 = Sum (FlattenSeq g1)
by POLYNOM1:14;
len (FlattenSeq g1) = len (prodTuples (p,q,r,(FlattenSeq g2)))
by A190, Def5;
then A235:
FlattenSeq g1 = prodTuples (
p,
q,
r,
(FlattenSeq g2))
by A193, FINSEQ_2:9;
len (FlattenSeq f1) = len (prodTuples (p,q,r,(FlattenSeq f2)))
by A217, Def5;
then
FlattenSeq f1 = prodTuples (
p,
q,
r,
(FlattenSeq f2))
by A219, FINSEQ_2:9;
then A236:
FlattenSeq f1 = (FlattenSeq g1) * P
by A235, A117, Th15;
len (Sum f1) = i + 1
by A1, A124, MATRLIN:def 6;
then
r1 = Sum f1
by A120, A127, FINSEQ_2:9;
then
Sum r1 = Sum (FlattenSeq f1)
by POLYNOM1:14;
hence
((p *' q) *' r) . i = (p *' (q *' r)) . i
by A121, A8, A234, A236, RLVECT_2:7;
verum end;
hence
(p *' q) *' r = p *' (q *' r)
; verum