let L be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 :: thesis: for i being Element of NAT holds ((p *' q) *' r) . i = (p *' (q *' r)) . i
let i be Element of NAT ; :: thesis: ((p *' q) *' r) . i = (p *' (q *' r)) . i
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
A1: len f2 = i + 1 and
A2: for k being Nat st k in dom f2 holds
f2 . k = H1(k) from A3: dom f2 = Seg (i + 1) by ;
reconsider f2 = f2 as FinSequence of () * ;
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 A6: dom g2 = Seg (i + 1) by ;
reconsider g2 = g2 as FinSequence of () * ;
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 ;
A11: dom (Card f2) = dom f2 by CARD_3:def 2
.= Seg (len g2) by
.= 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 :: thesis: for j being Nat st j in dom (Card f2) holds
(Card f2) . j = (Rev (Card g2)) . j
let j be Nat; :: thesis: ( 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) ; :: thesis: (Card f2) . j = (Rev (Card g2)) . j
then A15: j in Seg (len (Rev (Card g2))) by ;
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 ;
then A21: f2 . j = (Decomp ((j -' 1),2)) ^^ (j |-> <*((i + 1) -' j)*>) by A2, A3, A4;
i + 1 >= j by ;
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 ;
(i + 1) - (((i + 1) - j) + 1) = 0 + (j - 1) ;
then A23: (i + 1) - (((i + 1) - j) + 1) >= 0 by ;
then A24: ((i + 1) -' lj) + 1 = (0 + (j - 1)) + 1 by
.= j ;
((i + 1) - j) + 1 >= 0 + 1 by ;
then lj in Seg (i + 1) by ;
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
.= (i + (1 + 1)) - lj ;
A27: dom (((i + 2) -' lj) |-> <*(lj -' 1)*>) = Seg ((i + 2) -' lj) by FUNCOP_1:13
.= Seg j by ;
A28: dom (Decomp (((i + 1) -' lj),2)) = Seg (len (Decomp (((i + 1) -' lj),2))) by FINSEQ_1:def 3
.= Seg j by ;
Seg (len (g2 . lj)) = dom (g2 . lj) by FINSEQ_1:def 3
.= (Seg j) /\ (Seg j) by
.= 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 ;
Seg (len (f2 . j)) = dom (f2 . j) by FINSEQ_1:def 3
.= (Seg j) /\ (Seg j) by
.= Seg j ;
then A31: len (f2 . j) = j by FINSEQ_1:6;
((len (Card g2)) - j) + 1 in Seg (len g2) by ;
then A32: ((len (Card g2)) - j) + 1 in dom g2 by FINSEQ_1:def 3;
j in dom f2 by ;
hence (Card f2) . j = j by
.= (Card g2) . (((len (Card g2)) - j) + 1) by
.= (Rev (Card g2)) . j by ;
:: thesis: verum
end;
len (Card f2) = len (Rev (Card g2)) by ;
then A33: Card f2 = Rev (Card g2) by ;
reconsider w = Card g2 as FinSequence of NAT ;
A34: Seg (len ()) = dom () by FINSEQ_1:def 3;
now :: thesis: for y being object holds
( ( y in rng () implies y in rng () ) & ( y in rng () implies y in rng () ) )
let y be object ; :: thesis: ( ( y in rng () implies y in rng () ) & ( y in rng () implies y in rng () ) )
thus ( y in rng () implies y in rng () ) :: thesis: ( y in rng () implies y in rng () )
proof
assume y in rng () ; :: thesis: y in rng ()
then consider x being Nat such that
A35: x in dom () 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 = () . x by ;
A40: f2 . i1 = (Decomp ((i1 -' 1),2)) ^^ (i1 |-> <*((i + 1) -' i1)*>) by ;
then j1 in (dom (Decomp ((i1 -' 1),2))) /\ (dom (i1 |-> <*((i + 1) -' i1)*>)) by ;
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 ;
then A46: 1 <= i1 by FINSEQ_1:1;
then A47: j1 in Seg ((i1 -' 1) + 1) by ;
A48: i1 <= i + 1 by ;
then A49: (i + 1) - i1 >= 0 by XREAL_1:48;
A50: i + 1 >= j1 by ;
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 ;
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
.= (((i + 1) - j1) + 1) - ((1 - j1) + i1) by
.= (i + 1) -' i1 by ;
1 <= j1 by ;
then A54: j1 in Seg (i + 1) by ;
then A55: g2 . j1 = (((i + 2) -' j1) |-> <*(j1 -' 1)*>) ^^ (Decomp (((i + 1) -' j1),2)) by A5, A6;
i1 -' j1 <= (i + 1) -' j1 by ;
then ( 1 <= (i1 -' j1) + 1 & (i1 -' j1) + 1 <= ((i + 1) -' j1) + 1 ) by ;
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 ;
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 ;
then dom (g2 . j1) = (Seg ((i + 2) -' j1)) /\ (Seg ((i + 2) -' j1)) by ;
then A58: (i1 -' j1) + 1 in dom (g2 . j1) by ;
then A59: (g2 . j1) . ((i1 -' j1) + 1) = ((((i + 2) -' j1) |-> <*(j1 -' 1)*>) . ((i1 -' j1) + 1)) ^ ((Decomp (((i + 1) -' j1),2)) . ((i1 -' j1) + 1)) by
.= <*(j1 -' 1)*> ^ ((Decomp (((i + 1) -' j1),2)) . ((i1 -' j1) + 1)) by
.= <*(j1 -' 1)*> ^ <*(((i1 -' j1) + 1) -' 1),((((i + 1) -' j1) + 1) -' ((i1 -' j1) + 1))*> by
.= <*(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 ;
j1 in dom g2 by ;
then A60: ( (Sum (Card (g2 | (j1 -' 1)))) + ((i1 -' j1) + 1) in dom () & (g2 . j1) . ((i1 -' j1) + 1) = () . ((Sum (Card (g2 | (j1 -' 1)))) + ((i1 -' j1) + 1)) ) by ;
y = ((Decomp ((i1 -' 1),2)) . j1) ^ ((i1 |-> <*((i + 1) -' i1)*>) . j1) by
.= ((Decomp ((i1 -' 1),2)) . j1) ^ <*((i + 1) -' i1)*> by
.= <*(j1 -' 1),(((i1 -' 1) + 1) -' j1)*> ^ <*((i + 1) -' i1)*> by
.= <*(j1 -' 1),(i1 -' j1)*> ^ <*((i + 1) -' i1)*> by
.= <*(j1 -' 1),(i1 -' j1),((i + 1) -' i1)*> by FINSEQ_1:43 ;
hence y in rng () by ; :: thesis: verum
end;
assume y in rng () ; :: thesis: y in rng ()
then consider x being Nat such that
A61: x in dom () 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 = () . x by ;
A66: g2 . i1 = (((i + 2) -' i1) |-> <*(i1 -' 1)*>) ^^ (Decomp (((i + 1) -' i1),2)) by ;
then j1 in (dom (((i + 2) -' i1) |-> <*(i1 -' 1)*>)) /\ (dom (Decomp (((i + 1) -' i1),2))) by ;
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 ;
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 ;
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 ;
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 ;
(i + 1) - ((j1 - 1) + i1) >= 0 by ;
then (i + 1) - ((j1 -' 1) + i1) >= 0 by ;
then A76: (i + 1) -' ((j1 -' 1) + i1) = (i + 1) - ((j1 -' 1) + i1) by XREAL_0:def 2
.= (i + 1) - ((j1 - 1) + i1) by
.= (((i + 1) - i1) + 1) - j1
.= (((i + 1) -' i1) + 1) - j1 by
.= (((i + 1) -' i1) + 1) -' j1 by ;
A77: y = ((((i + 2) -' i1) |-> <*(i1 -' 1)*>) . j1) ^ ((Decomp (((i + 1) -' i1),2)) . j1) by
.= <*(i1 -' 1)*> ^ ((Decomp (((i + 1) -' i1),2)) . j1) by
.= <*(i1 -' 1)*> ^ <*(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by
.= <*(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 ;
then A81: i1 in Seg ((j1 -' 1) + i1) by ;
then A82: i1 in Seg ((((j1 -' 1) + i1) -' 1) + 1) by ;
(j1 -' 1) + i1 >= 1 by ;
then A83: (j1 -' 1) + i1 in Seg (i + 1) by ;
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 ;
then dom (f2 . ((j1 -' 1) + i1)) = (Seg ((j1 -' 1) + i1)) /\ (Seg ((j1 -' 1) + i1)) by ;
then A85: i1 in dom (f2 . ((j1 -' 1) + i1)) by ;
(j1 -' 1) + i1 in dom f2 by ;
then A86: ( (Sum (Card (f2 | (((j1 -' 1) + i1) -' 1)))) + i1 in dom () & (f2 . ((j1 -' 1) + i1)) . i1 = () . ((Sum (Card (f2 | (((j1 -' 1) + i1) -' 1)))) + i1) ) by ;
(f2 . ((j1 -' 1) + i1)) . i1 = ((Decomp ((((j1 -' 1) + i1) -' 1),2)) . i1) ^ ((((j1 -' 1) + i1) |-> <*((i + 1) -' ((j1 -' 1) + i1))*>) . i1) by
.= ((Decomp ((((j1 -' 1) + i1) -' 1),2)) . i1) ^ <*((i + 1) -' ((j1 -' 1) + i1))*> by
.= <*(i1 -' 1),(((((j1 -' 1) + i1) -' 1) + 1) -' i1)*> ^ <*((i + 1) -' ((j1 -' 1) + i1))*> by
.= <*(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
.= <*(i1 -' 1),(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by ;
hence y in rng () by ; :: thesis: verum
end;
then A87: rng () = rng () by TARSKI:2;
now :: thesis: for x, y being object st x in dom () & y in dom () & () . x = () . y holds
x = y
A88: (i + 1) + 1 >= i + 1 by NAT_1:11;
let x, y be object ; :: thesis: ( x in dom () & y in dom () & () . x = () . y implies x = y )
assume that
A89: x in dom () and
A90: y in dom () and
A91: (FlattenSeq g2) . x = () . y ; :: thesis: x = y
consider 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 = () . x by ;
A96: g2 . i1 = (((i + 2) -' i1) |-> <*(i1 -' 1)*>) ^^ (Decomp (((i + 1) -' i1),2)) by ;
i1 in Seg (i + 1) by ;
then A97: i1 <= i + 1 by FINSEQ_1:1;
then (i + 1) + 1 >= i1 by ;
then A98: (i + 2) - i1 >= 0 by XREAL_1:48;
(i + 1) - i1 >= 0 by ;
then A99: ((i + 1) -' i1) + 1 = ((i + 1) - i1) + 1 by XREAL_0:def 2
.= (i + 2) -' i1 by ;
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 ;
then A101: dom (g2 . i1) = (Seg ((i + 2) -' i1)) /\ (Seg ((i + 2) -' i1)) by
.= Seg ((i + 2) -' i1) ;
j1 in Seg (len (g2 . i1)) by ;
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 = () . y by ;
A107: g2 . i2 = (((i + 2) -' i2) |-> <*(i2 -' 1)*>) ^^ (Decomp (((i + 1) -' i2),2)) by ;
i2 in Seg (i + 1) by ;
then A108: i2 <= i + 1 by FINSEQ_1:1;
then (i + 1) + 1 >= i2 by ;
then A109: (i + 2) - i2 >= 0 by XREAL_1:48;
(i + 1) - i2 >= 0 by ;
then A110: ((i + 1) -' i2) + 1 = ((i + 1) - i2) + 1 by XREAL_0:def 2
.= (i + 2) -' i2 by ;
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 ;
then A112: dom (g2 . i2) = (Seg ((i + 2) -' i2)) /\ (Seg ((i + 2) -' i2)) by
.= Seg ((i + 2) -' i2) ;
A113: (g2 . i2) . j2 = ((((i + 2) -' i2) |-> <*(i2 -' 1)*>) . j2) ^ ((Decomp (((i + 1) -' i2),2)) . j2) by
.= <*(i2 -' 1)*> ^ ((Decomp (((i + 1) -' i2),2)) . j2) by
.= <*(i2 -' 1)*> ^ <*(j2 -' 1),((((i + 1) -' i2) + 1) -' j2)*> by
.= <*(i2 -' 1),(j2 -' 1),((((i + 1) -' i2) + 1) -' j2)*> by FINSEQ_1:43 ;
j2 in Seg (len (g2 . i2)) by ;
then A114: j2 >= 1 by FINSEQ_1:1;
(g2 . i1) . j1 = ((((i + 2) -' i1) |-> <*(i1 -' 1)*>) . j1) ^ ((Decomp (((i + 1) -' i1),2)) . j1) by
.= <*(i1 -' 1)*> ^ ((Decomp (((i + 1) -' i1),2)) . j1) by
.= <*(i1 -' 1)*> ^ <*(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by
.= <*(i1 -' 1),(j1 -' 1),((((i + 1) -' i1) + 1) -' j1)*> by FINSEQ_1:43 ;
then ( i1 -' 1 = i2 -' 1 & j1 -' 1 = j2 -' 1 ) by ;
hence x = y by ; :: thesis: verum
end;
then A115: FlattenSeq g2 is one-to-one by FUNCT_1:def 4;
A116: w is FinSequence of REAL by ;
len () = Sum (Card f2) by PRE_POLY:27
.= Sum w by
.= len () by PRE_POLY:27 ;
then FlattenSeq f2 is one-to-one by ;
then FlattenSeq f2, FlattenSeq g2 are_fiberwise_equipotent by ;
then consider P being Permutation of (dom ()) such that
A117: FlattenSeq f2 = () * 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 ;
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 A126: dom f1 = Seg (len f2) by ;
A127: now :: thesis: for j being Nat st j in dom r1 holds
r1 . j = (Sum f1) . j
let j be Nat; :: thesis: ( 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 ; :: thesis: r1 . j = (Sum f1) . j
then A133: 1 <= j by ;
then A134: len r3 = j by ;
len (Decomp ((j -' 1),2)) = (j -' 1) + 1 by Th9
.= j by ;
then A135: dom (Decomp ((j -' 1),2)) = Seg j by FINSEQ_1:def 3;
A136: dom r1 = dom f1 by ;
then A137: f1 /. j = f1 . j by
.= prodTuples (p,q,r,(f2 /. j)) by ;
dom f1 = dom f2 by ;
then A138: f2 /. j = f2 . j by
.= (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 ;
A140: len (prodTuples (p,q,r,(f2 /. j))) = len (f2 /. j) by Def5
.= j by ;
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 :: thesis: 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))) . k
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 A144: k in dom (prodTuples (p,q,r,(f2 /. j))) ; :: thesis: (prodTuples (p,q,r,(f2 /. j))) . k = (r3 * (r . ((i + 1) -' j))) . k
then A145: (f2 /. j) /. k = (f2 /. j) . k by
.= ((Decomp ((j -' 1),2)) . k) ^ ((j |-> <*((i + 1) -' j)*>) . k) by
.= <*(k -' 1),(((j -' 1) + 1) -' k)*> ^ ((j |-> <*((i + 1) -' j)*>) . k) by
.= <*(k -' 1),(((j -' 1) + 1) -' k)*> ^ <*((i + 1) -' j)*> by
.= <*(k -' 1),(((j -' 1) + 1) -' k),((i + 1) -' j)*> by FINSEQ_1:43 ;
1 in Seg 3 by ;
then 1 in Seg (len ((f2 /. j) /. k)) by ;
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 ;
A147: k in dom r3 by ;
then A148: r3 /. k = r3 . k by PARTFUN1:def 6
.= (p . (k -' 1)) * (q . (((j -' 1) + 1) -' k)) by ;
3 in Seg 3 by ;
then 3 in Seg (len ((f2 /. j) /. k)) by ;
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 ;
2 in Seg 3 by ;
then 2 in Seg (len ((f2 /. j) /. k)) by ;
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 ;
thus (prodTuples (p,q,r,(f2 /. j))) . k = ((p . (((f2 /. j) /. k) /. 1)) * (q . (((f2 /. j) /. k) /. 2))) * (r . (((f2 /. j) /. k) /. 3)) by
.= (r3 * (r . ((i + 1) -' j))) /. k by
.= (r3 * (r . ((i + 1) -' j))) . k by ; :: thesis: 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 ;
then A152: prodTuples (p,q,r,(f2 /. j)) = r3 * (r . ((i + 1) -' j)) by ;
((p *' q) . (j -' 1)) * (r . ((i + 1) -' j)) = Sum (r3 * (r . ((i + 1) -' j))) by ;
hence r1 . j = Sum (r3 * (r . ((i + 1) -' j))) by
.= (Sum f1) /. j by
.= (Sum f1) . j by ;
:: thesis: 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 A155: dom g1 = Seg (len g2) by ;
A156: now :: thesis: for j being Nat st j in dom r2 holds
r2 . j = (Sum g1) . j
let j be Nat; :: thesis: ( 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 ; :: thesis: r2 . j = (Sum g1) . j
then A162: j <= i + 1 by ;
(i + 1) + 1 >= i + 1 by NAT_1:11;
then (i + 1) + 1 >= j by ;
then A163: (i + 2) - j >= 0 by XREAL_1:48;
(i + 1) - j >= 0 by ;
then A164: ((i + 1) -' j) + 1 = ((i + 1) - j) + 1 by XREAL_0:def 2
.= (i + 2) -' j by ;
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 ;
then A167: g1 /. j = g1 . j by
.= prodTuples (p,q,r,(g2 /. j)) by ;
dom g1 = dom g2 by ;
then A168: g2 /. j = g2 . j by
.= (((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 ;
A170: len (prodTuples (p,q,r,(g2 /. j))) = len (g2 /. j) by Def5
.= (i + 2) -' j by ;
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 :: thesis: 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) . k
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 A174: k in dom (prodTuples (p,q,r,(g2 /. j))) ; :: thesis: (prodTuples (p,q,r,(g2 /. j))) . k = ((p . (j -' 1)) * r3) . k
then A175: (g2 /. j) /. k = (g2 /. j) . k by
.= ((((i + 2) -' j) |-> <*(j -' 1)*>) . k) ^ ((Decomp (((i + 1) -' j),2)) . k) by
.= ((((i + 2) -' j) |-> <*(j -' 1)*>) . k) ^ <*(k -' 1),((((i + 1) -' j) + 1) -' k)*> by
.= <*(j -' 1)*> ^ <*(k -' 1),((((i + 1) -' j) + 1) -' k)*> by
.= <*(j -' 1),(k -' 1),((((i + 1) -' j) + 1) -' k)*> by FINSEQ_1:43 ;
1 in Seg 3 by ;
then 1 in Seg (len ((g2 /. j) /. k)) by ;
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 ;
A177: k in dom r3 by ;
then A178: r3 /. k = r3 . k by PARTFUN1:def 6
.= (q . (k -' 1)) * (r . ((((i + 1) -' j) + 1) -' k)) by ;
3 in Seg 3 by ;
then 3 in Seg (len ((g2 /. j) /. k)) by ;
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 ;
2 in Seg 3 by ;
then 2 in Seg (len ((g2 /. j) /. k)) by ;
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 ;
thus (prodTuples (p,q,r,(g2 /. j))) . k = ((p . (((g2 /. j) /. k) /. 1)) * (q . (((g2 /. j) /. k) /. 2))) * (r . (((g2 /. j) /. k) /. 3)) by
.= (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
.= ((p . (j -' 1)) * r3) . k by ; :: thesis: 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 ;
then A182: prodTuples (p,q,r,(g2 /. j)) = (p . (j -' 1)) * r3 by ;
(p . (j -' 1)) * ((q *' r) . ((i + 1) -' j)) = Sum ((p . (j -' 1)) * r3) by ;
hence r2 . j = Sum ((p . (j -' 1)) * r3) by
.= (Sum g1) /. j by
.= (Sum g1) . j by ;
:: thesis: verum
end;
A183: dom (Card g2) = Seg (i + 1) by ;
A184: now :: thesis: for j being Nat st j in dom (Card g2) holds
(Card g2) . j = (Card g1) . j
let j be Nat; :: thesis: ( j in dom (Card g2) implies (Card g2) . j = (Card g1) . j )
assume A185: j in dom (Card g2) ; :: thesis: (Card g2) . j = (Card g1) . j
then A186: j in dom g1 by ;
g1 . j = prodTuples (p,q,r,(g2 /. j)) by ;
then A187: len (g1 . j) = len (g2 /. j) by Def5
.= len (g2 . j) by ;
thus (Card g2) . j = len (g2 . j) by
.= (Card g1) . j by ; :: thesis: 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 ;
then A190: len () = len () by PRE_POLY:28;
then A191: dom () = dom () by FINSEQ_3:29;
then reconsider P = P as Permutation of (dom ()) ;
A192: dom () = Seg (len ()) by FINSEQ_1:def 3;
A193: now :: thesis: for j being Nat st j in dom () holds
() . j = (prodTuples (p,q,r,())) . j
let j be Nat; :: thesis: ( j in dom () implies () . j = (prodTuples (p,q,r,())) . j )
assume A194: j in dom () ; :: thesis: () . j = (prodTuples (p,q,r,())) . j
then 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 = () . j by PRE_POLY:29;
A199: j in dom () by ;
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 = () . 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 ;
then A203: ( i1 = i2 & j1 = j2 ) by ;
i1 in Seg (len g2) by ;
then A204: i1 in dom g2 by FINSEQ_1:def 3;
A205: g1 . i1 = prodTuples (p,q,r,(g2 /. i1)) by ;
then len (g1 . i1) = len (g2 /. i1) by Def5
.= len (g2 . i1) by ;
then j1 in Seg (len (g2 . i1)) by ;
then A206: j1 in Seg (len (g2 /. i1)) by ;
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
.= () /. j by ;
Seg (len (g2 /. i1)) = dom (g2 /. i1) by FINSEQ_1:def 3;
hence () . j = ((p . (((g2 /. i1) /. j1) /. 1)) * (q . (((g2 /. i1) /. j1) /. 2))) * (r . (((g2 /. i1) /. j1) /. 3)) by
.= (prodTuples (p,q,r,())) . j by ;
:: thesis: 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 ;
A211: now :: thesis: for j being Nat st j in dom (Card f2) holds
(Card f2) . j = (Card f1) . j
let j be Nat; :: thesis: ( j in dom (Card f2) implies (Card f2) . j = (Card f1) . j )
assume A212: j in dom (Card f2) ; :: thesis: (Card f2) . j = (Card f1) . j
then A213: j in dom f1 by ;
f1 . j = prodTuples (p,q,r,(f2 /. j)) by ;
then A214: len (f1 . j) = len (f2 /. j) by Def5
.= len (f2 . j) by ;
thus (Card f2) . j = len (f2 . j) by
.= (Card f1) . j by ; :: thesis: 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 ;
then A217: len () = len () by PRE_POLY:28;
A218: Seg (len ()) = dom () by FINSEQ_1:def 3;
A219: now :: thesis: for j being Nat st j in dom () holds
() . j = (prodTuples (p,q,r,())) . j
let j be Nat; :: thesis: ( j in dom () implies () . j = (prodTuples (p,q,r,())) . j )
assume A220: j in dom () ; :: thesis: () . j = (prodTuples (p,q,r,())) . j
then 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 = () . j by PRE_POLY:29;
A225: j in dom () by ;
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 = () . 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 ;
then A229: ( i1 = i2 & j1 = j2 ) by ;
i1 in Seg (len f2) by ;
then A230: i1 in dom f2 by FINSEQ_1:def 3;
A231: f1 . i1 = prodTuples (p,q,r,(f2 /. i1)) by ;
then len (f1 . i1) = len (f2 /. i1) by Def5
.= len (f2 . i1) by ;
then j1 in Seg (len (f2 . i1)) by ;
then A232: j1 in Seg (len (f2 /. i1)) by ;
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
.= () /. j by ;
Seg (len (f2 /. i1)) = dom (f2 /. i1) by FINSEQ_1:def 3;
hence () . j = ((p . (((f2 /. i1) /. j1) /. 1)) * (q . (((f2 /. i1) /. j1) /. 2))) * (r . (((f2 /. i1) /. j1) /. 3)) by
.= ((p . ((() /. j) /. 1)) * (q . ((() /. j) /. 2))) * (r . ((() /. j) /. 3)) by A233
.= (prodTuples (p,q,r,())) . j by ;
:: thesis: verum
end;
len (Sum g1) = i + 1 by ;
then r2 = Sum g1 by ;
then A234: Sum r2 = Sum () by POLYNOM1:14;
len () = len (prodTuples (p,q,r,())) by ;
then A235: FlattenSeq g1 = prodTuples (p,q,r,()) by ;
len () = len (prodTuples (p,q,r,())) by ;
then FlattenSeq f1 = prodTuples (p,q,r,()) by ;
then A236: FlattenSeq f1 = () * P by ;
len (Sum f1) = i + 1 by ;
then r1 = Sum f1 by ;
then Sum r1 = Sum () by POLYNOM1:14;
hence ((p *' q) *' r) . i = (p *' (q *' r)) . i by ; :: thesis: verum
end;
hence (p *' q) *' r = p *' (q *' r) ; :: thesis: verum