:: Binary Operations on Finite Sequences
:: by Wojciech A. Trybulec
::
:: Received August 10, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, FINSEQ_1, FUNCT_1, BINOP_1, FUNCT_2,
RELAT_1, FINSEQ_2, SETWISEO, XXREAL_0, CARD_1, ARYTM_3, FUNCOP_1, TARSKI,
FUNCT_4, FINSUB_1, ORDINAL4, NAT_1, ARYTM_1, PARTFUN1, FINSOP_1, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, BINOP_1,
PARTFUN1, FINSEQ_2, FINSEQ_1, FINSEQ_4, RELAT_1, RELSET_1, FUNCT_1,
FINSUB_1, SETWISEO, FUNCT_2, NAT_1, FUNCOP_1, FUNCT_4, XXREAL_0;
constructors BINOP_1, PARTFUN1, FUNCOP_1, FUNCT_4, SETWISEO, XXREAL_0,
XREAL_0, NAT_1, FINSEQ_2, FINSEQ_4, RELSET_1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, XXREAL_0,
XREAL_0, FINSEQ_1, CARD_1, FINSEQ_2, NAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FUNCT_1, TARSKI, XBOOLE_0;
theorems BINOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCT_1, FUNCT_2,
NAT_1, SETWISEO, TARSKI, RELAT_1, FUNCOP_1, FUNCT_4, FINSUB_1, RELSET_1,
XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1;
schemes FINSEQ_1, FINSEQ_2, NAT_1, FUNCT_2;
begin
reserve x,y,y1,y2 for set,
D for non empty set,
d,d1,d2,d3 for Element of D,
F,G,H,H1,H2 for FinSequence of D,
f,f1,f2 for sequence of D,
g for BinOp of D,
k,n,i,l for Nat,
P for Permutation of dom F;
definition
let D;
let F be D-valued FinSequence;
let g be BinOp of D;
assume
A1: g is having_a_unity or len F >= 1;
func g "**" F -> Element of D means
:Def1:
it = the_unity_wrt g if g is having_a_unity & len F = 0
otherwise
ex f st f.1 = F.1 &
(for n being Nat st 0 <> n & n < len F holds f.(n + 1) = g.(f.n,F.(n + 1)))
& it = f.(len F);
existence
proof
now
per cases;
suppose
len F = 0;
hence thesis by A1;
end;
suppose
A2: len F <> 0;
defpred P[Nat] means
for F being D-valued FinSequence st len F = $1 & len F <> 0
ex d,f st f.1 = F.1 &
(for n being Nat st 0 <> n & n < len F
holds f.(n + 1) = g.(f.n,F.(n + 1))) & d = f.(len F);
A3: for k st P[k] holds P[k + 1]
proof
let k;
assume
A4: P[k];
let F be D-valued FinSequence;
assume that
A5: len F = k + 1 and
len F <> 0;
reconsider G = F | Seg k as FinSequence of D by FINSEQ_1:18;
A6: len G = k by A5,FINSEQ_3:53;
now
per cases;
suppose
A7: len G = 0;
set f = NAT --> F.1;
A8: rng f c= D
proof
let x be object;
assume x in rng f;
then ex y being object st y in dom f & f.y = x
by FUNCT_1:def 3;
then
A9: x = F.1 by FUNCOP_1:7;
1 in dom F by A5,A6,A7,FINSEQ_3:25;
then
A10: x in rng F by A9,FUNCT_1:def 3;
rng F c= D by RELAT_1:def 19;
hence thesis by A10;
end;
dom f = NAT by FUNCOP_1:13;
then reconsider f as sequence of D by A8,RELSET_1:4;
take d = f.1,f;
thus f.1 = F.1 by FUNCOP_1:7;
thus for n being Nat st 0 <> n & n < len F
holds f.(n + 1) = g.(f.n,F.(n +1)) by A5,A6,A7,NAT_1:14;
thus d = f.(len F) by A5,A6,A7;
end;
suppose
A11: len G <> 0;
reconsider j = len F as Element of NAT;
1 <= len F by A5,NAT_1:12;
then len F in dom F by FINSEQ_3:25;
then
A12: F.(len F) in rng F by FUNCT_1:def 3;
rng F c= D by RELAT_1:def 19;
then reconsider t = F.(len F) as Element of D by A12;
len G >= 1 by A11,NAT_1:14;
then
A13: 1 in dom G by FINSEQ_3:25;
consider d,f such that
A14: f.1 = G.1 and
A15: for n being Nat st 0 <> n & n < len G
holds f.(n + 1) = g.(f.n,G.
(n + 1)) and
A16: d = f.(len G) by A4,A5,A11,FINSEQ_3:53;
deffunc F(Element of NAT) = f.$1;
consider h being sequence of D such that
A17: h.j = g.(d,t) and
A18: for n being Element of NAT st n <> j holds h.n = F(n)
from FUNCT_2:sch 6;
take a = h.j,h;
1 <> j by A5,A11,FINSEQ_3:53;
hence h.1 = G.1 by A14,A18
.= F.1 by A13,FUNCT_1:47;
thus for n being Nat st 0 <> n & n < len F
holds h.(n + 1) = g.(h.n,F.(n +1))
proof
let n be Nat;
assume that
A19: n <> 0 and
A20: n < len F;
now
per cases;
suppose
A21: n + 1 = len F;
len G <> len F by A5,A6;
hence thesis by A5,A6,A16,A17,A18,A21;
end;
suppose
A22: n + 1 <> len F;
n + 1 <= len F by A20,NAT_1:13;
then
A23: n + 1 < len F by A22,XXREAL_0:1;
then
A24: n < len G by A5,A6,XREAL_1:6;
1 <= n + 1 & n + 1 <= len G by A5,A6,A23,NAT_1:12,13;
then
A25: n + 1 in dom G by FINSEQ_3:25;
h.(n + 1) = f.(n + 1) by A18,A22
.= g.(f.n,G.(n + 1)) by A15,A19,A24
.= g.(f.n,F.(n + 1)) by A25,FUNCT_1:47
.= g.(h.In(n,NAT),F.(n + 1)) by A18,A20;
hence thesis;
end;
end;
hence thesis;
end;
thus a = h.(len F);
end;
end;
hence thesis;
end;
A26: P[0];
for k holds P[k] from NAT_1:sch 2(A26,A3);
hence thesis by A2;
end;
end;
hence thesis;
end;
uniqueness
proof
let d1,d2;
thus g is having_a_unity & len F = 0 & d1 = the_unity_wrt g & d2 =
the_unity_wrt g implies d1 = d2;
assume
A27: not g is having_a_unity or len F <> 0;
given f1 such that
A28: f1.1 = F.1 and
A29: for n being Nat st 0 <> n & n < len F
holds f1.(n + 1) = g.(f1.n,F.(n + 1)) and
A30: d1 = f1.(len F);
given f2 such that
A31: f2.1 = F.1 and
A32: for n being Nat st 0 <> n & n < len F
holds f2.(n + 1) = g.(f2.n,F.(n + 1)) and
A33: d2 = f2.(len F);
defpred P[Nat] means $1 <> 0 & $1 <= len F implies f1.$1 = f2.$1;
A34: for n st P[n] holds P[n + 1]
proof
let n;
assume
A35: n <> 0 & n <= len F implies f1.n = f2.n;
assume that
n + 1 <> 0 and
A36: n + 1 <= len F;
now
per cases;
suppose
n = 0;
hence thesis by A28,A31;
end;
suppose
A37: n <> 0;
A38: n < len F by A36,NAT_1:13;
then f1.(n + 1) = g.(f1.n,F.(n + 1)) by A29,A37;
hence thesis by A32,A35,A37,A38;
end;
end;
hence thesis;
end;
A39: P[0];
for n holds P[n] from NAT_1:sch 2(A39,A34);
hence thesis by A1,A27,A30,A33;
end;
consistency;
end;
theorem
len F >= 1 implies ex f st f.1 = F.1 &
(for n being Nat st 0 <> n & n < len F
holds f.(n + 1) = g.(f.n,F.(n + 1))) & g "**" F = f.(len F) by Def1;
theorem
len F >= 1 & (ex f st f.1 = F.1 &
(for n being Nat st 0 <> n & n < len F holds f
.(n + 1) = g.(f.n,F.(n + 1))) & d = f.(len F)) implies d = g "**" F by Def1;
definition
let A be non empty set, F be sequence of A, p be FinSequence of A;
redefine func F +* p -> sequence of A; :: redefines +* (FUNCT_4, definition)
coherence
proof
A1: dom F = NAT by FUNCT_2:def 1;
dom(F +* p) = dom F \/ dom p by FUNCT_4:def 1
.= NAT by A1,XBOOLE_1:12;
hence thesis by FUNCT_2:def 1;
end;
end;
notation
let f be FinSequence;
synonym findom↑ f for dom f;
end;
definition
let f be FinSequence;
redefine func findom f -> Element of Fin NAT; :: redefines findom (FINSOP_1, synonym) → dom (RELAT_1, synonym) → proj1 (XTUPLE_0, definition)
coherence
proof
dom f = Seg len f by FINSEQ_1:def 3;
hence thesis by FINSUB_1:def 5;
end;
end;
Lm1: len F >= 1 & g is associative & g is commutative implies g "**" F = g $$(
findom F,(NAT-->the_unity_wrt g)+*F)
proof
assume that
A1: len F >= 1 and
A2: g is associative & g is commutative;
set A = findom F;
set h = (NAT-->the_unity_wrt g)+*F;
A3: dom F = Seg len F by FINSEQ_1:def 3;
then consider G being Function of Fin NAT,D such that
A4: g $$ (A,h) = G.A and
for d st d is_a_unity_wrt g holds G.{} = d and
A5: for n being Element of NAT holds G.{n} = h.n and
A6: for B being Element of Fin NAT st B c= A & B <> {}
for n being Element of NAT st n in A \ B
holds G.(B \/ {n}) = g.(G.B,h.n) by A1,A2,SETWISEO:def 3;
consider f such that
A7: f.1 = F.1 and
A8: for n being Nat st 0 <> n & n < len F
holds f.(n + 1) = g.(f.n,F.(n + 1)) and
A9: g "**" F = f.(len F) by A1,Def1;
defpred P[Nat] means $1 <> 0 & $1 <= len F implies f.$1 = G.(Seg $1);
A10: for n st P[n] holds P[n + 1]
proof
let n;
assume
A11: n <> 0 & n <= len F implies f.n = G.(Seg n);
assume that
n + 1 <> 0 and
A12: n + 1 <= len F;
now
per cases;
suppose
A13: n = 0;
1 in dom F by A1,A3,FINSEQ_1:1;
then h.1 = F.1 by FUNCT_4:13;
hence thesis by A7,A5,A13,FINSEQ_1:2;
end;
suppose
A14: n <> 0;
reconsider B = Seg n as Element of Fin NAT by FINSUB_1:def 5;
n + 1 >= 1 by NAT_1:12;
then
A15: n + 1 in dom F by A12,FINSEQ_3:25;
A16: n < len F by A12,NAT_1:13;
then
A17: f.(n + 1) = g.(f.n,F.(n + 1)) by A8,A14;
not n + 1 in Seg n by FINSEQ_3:10;
then
A18: n + 1 in A \ Seg n by A15,XBOOLE_0:def 5;
A19: Seg n c= A by A3,A16,FINSEQ_1:5;
G.(Seg(n + 1)) = G.(Seg n \/ {n + 1}) by FINSEQ_1:9
.= g.(G.B,h.(n + 1)) by A6,A14,A19,A18;
hence thesis by A11,A12,A14,A17,A15,FUNCT_4:13,NAT_1:13;
end;
end;
hence thesis;
end;
A20: P[0];
for n holds P[n] from NAT_1:sch 2(A20,A10);
hence thesis by A1,A9,A3,A4;
end;
Lm2: len F = 0 & g is having_a_unity & g is associative & g is commutative
implies g "**" F = g $$(findom F,(NAT-->the_unity_wrt g)+*F)
proof
assume that
A1: len F = 0 and
A2: g is having_a_unity and
A3: g is associative & g is commutative;
F = {} by A1;
then
A4: dom F = {}.NAT;
thus g "**" F = the_unity_wrt g by A1,A2,Def1
.= g $$(findom F,(NAT-->the_unity_wrt g)+*F) by A2,A3,A4,SETWISEO:31;
end;
theorem
(g is having_a_unity or len F >= 1) & g is associative & g is
commutative implies g "**" F = g $$(findom F,(NAT-->the_unity_wrt g)+*F)
proof
len F = 0 or len F >= 1 by NAT_1:14;
hence thesis by Lm1,Lm2;
end;
Lm3: g is having_a_unity implies g "**" <*>D = the_unity_wrt g
proof
A1: len <*>D = 0;
assume g is having_a_unity;
hence thesis by A1,Def1;
end;
Lm4: g "**" <* d *> = d
proof
A1: len<* d *> = 1 by FINSEQ_1:39;
then
ex f st f.1 = <* d *>.1 &
(for n being Nat st 0 <> n & n < len<* d *> holds f.(n +
1) = g.(f.n,<* d *>.(n + 1))) & g "**" <* d *> = f.len<* d *> by Def1;
hence thesis by A1;
end;
Lm5: len F >= 1 implies g "**" (F ^ <* d *>) = g.(g "**" F,d)
proof
set G = F ^ <* d *>;
A1: G.(len F + 1) = d by FINSEQ_1:42;
A2: len G = len F + len<* d *> by FINSEQ_1:22
.= len F + 1 by FINSEQ_1:39;
then 1 <= len G by NAT_1:12;
then consider f1 such that
A3: f1.1 = G.1 and
A4: for n being Nat st 0 <> n & n < len G
holds f1.(n + 1) = g.(f1.n,G.(n + 1)) and
A5: g "**" G = f1.(len G) by Def1;
assume
A6: len F >= 1;
then consider f such that
A7: f.1 = F.1 and
A8: for n being Nat st 0 <> n & n < len F
holds f.(n + 1) = g.(f.n,F.(n + 1)) and
A9: g "**" F = f.(len F) by Def1;
defpred P[Nat] means 0 <> $1 & $1 < len G implies f.$1 = f1.$1;
A10: for n st P[n] holds P[n + 1]
proof
let n;
assume
A11: P[n];
assume that
0 <> n + 1 and
A12: n + 1 < len G;
A13: n + 1 >= 1 by NAT_1:14;
now
per cases by A13,XXREAL_0:1;
suppose
A14: n + 1 = 1;
1 in dom F by A6,FINSEQ_3:25;
hence thesis by A7,A3,A14,FINSEQ_1:def 7;
end;
suppose
A15: n + 1 > 1;
then n <> 0;
then
A16: f1.(n + 1) = g.(f1.n,G.(n + 1)) by A4,A12,NAT_1:12;
A17: n + 1 <= len F by A2,A12,NAT_1:13;
then
A18: n < len F by NAT_1:13;
1 <= n + 1 by NAT_1:12;
then
A19: n + 1 in dom F by A17,FINSEQ_3:25;
n + 1 > 0 + 1 by A15;
then f.(n + 1) = g.(f.n,F.(n + 1)) by A8,A18;
hence thesis by A11,A12,A15,A16,A19,FINSEQ_1:def 7,NAT_1:12;
end;
end;
hence thesis;
end;
A20: P[0];
A21: for n holds P[n] from NAT_1:sch 2(A20,A10);
g "**" G = g.(f1.(len F),G.(len F + 1)) by A6,A2,A4,A5,XREAL_1:29;
hence thesis by A6,A9,A2,A1,A21,XREAL_1:29;
end;
Lm6: g is having_a_unity & len F = 0 implies g "**" (F ^ <* d *>) = g.(g "**"
F,d)
proof
assume that
A1: g is having_a_unity and
A2: len F = 0;
F = <*>D by A2;
hence g "**" (F ^ <* d *>) = g "**" <* d *> by FINSEQ_1:34
.= d by Lm4
.= g.(the_unity_wrt g,d) by A1,SETWISEO:15
.= g.(g "**" F,d) by A1,A2,Def1;
end;
theorem Th4:
g is having_a_unity or len F >= 1 implies g "**" (F ^ <* d *>) =
g.(g "**" F,d)
proof
len F >= 1 or len F = 0 by NAT_1:14;
hence thesis by Lm5,Lm6;
end;
theorem Th5:
g is associative & (g is having_a_unity or len F >= 1 & len G >=
1) implies g "**" (F ^ G) = g.(g "**" F,g "**" G)
proof
defpred P[FinSequence of D] means for F,g st g is associative & (g is
having_a_unity or len F >= 1 & len $1 >= 1) holds g "**" (F ^ $1) = g.(g "**" F
,g "**" $1);
A1: for G,d st P[G] holds P[G ^ <* d *>]
proof
let G,d;
assume
A2: P[G];
let F,g;
assume that
A3: g is associative and
A4: g is having_a_unity or len F >= 1 & len(G ^ <* d *>) >= 1;
A5: now
A6: len(F ^ G) = len F + len G by FINSEQ_1:22;
assume not g is having_a_unity;
hence len(F ^ G) >= 1 by A4,A6,NAT_1:12;
end;
A7: g "**" (F ^ (G ^ <* d *>)) = g "**" (F ^ G ^ <* d *>) by FINSEQ_1:32
.= g.(g "**" (F ^ G),d) by A5,Th4;
now
per cases;
suppose
A8: len G <> 0;
then len G >= 1 by NAT_1:14;
hence
g "**" (F ^ (G ^ <* d *>)) = g.(g.(g "**" F,g "**" G),d) by A2,A3,A4,A7
.= g.(g "**" F,g.(g "**" G,d)) by A3,BINOP_1:def 3
.= g.(g "**" F,g "**" (G ^ <* d *>)) by A8,Th4,NAT_1:14;
end;
suppose
len G = 0;
then
A9: G = {};
hence g "**" (F ^ (G ^ <* d *>)) = g "**" (F ^ <* d *>) by FINSEQ_1:34
.= g.(g "**" F,d) by A4,Th4
.= g.(g "**" F,g "**" <* d *>) by Lm4
.= g.(g "**" F,g "**" (G ^ <* d *>)) by A9,FINSEQ_1:34;
end;
end;
hence thesis;
end;
A10: P[<*>D]
proof
let F,g;
assume that
g is associative and
A11: g is having_a_unity or len F >= 1 & len <*>D >= 1;
thus g "**" (F ^ <*>D) = g "**" F by FINSEQ_1:34
.= g.(g "**" F,the_unity_wrt g) by A11,SETWISEO:15
.= g.(g "**" F,g "**" <*>D) by A11,Lm3;
end;
for G holds P[G] from FINSEQ_2:sch 2(A10,A1);
hence thesis;
end;
theorem Th6:
g is associative & (g is having_a_unity or len F >= 1) implies g
"**" (<* d *> ^ F) = g.(d,g "**" F)
proof
A1: len<* d *> = 1 by FINSEQ_1:39;
assume g is associative &( g is having_a_unity or len F >= 1);
hence g "**" (<* d *> ^ F) = g.(g "**" <* d *>,g "**" F) by A1,Th5
.= g.(d,g "**" F) by Lm4;
end;
Lm7: g is associative & g is commutative implies for f being Permutation of
dom F st len F >= 1 & len F = len G & (for i st i in dom G holds G.i = F.(f.i))
holds g "**" F = g "**" G
proof
assume that
A1: g is associative and
A2: g is commutative;
defpred P[Nat] means for H1,H2 st len H1 >= 1 & len H1 = $1 & len
H1 = len H2 for f being Permutation of dom H1 st (for i st i in dom H2 holds H2
.i = H1.(f.i)) holds g "**" H1 = g "**" H2;
A3: now
let k;
assume
A4: P[k];
thus P[k+1]
proof
let H1,H2;
assume that
len H1 >= 1 and
A5: len H1 = k + 1 and
A6: len H1 = len H2;
reconsider p = H2 | (Seg k) as FinSequence of D by FINSEQ_1:18;
let f be Permutation of dom H1;
A7: dom H1 = Seg(k + 1) by A5,FINSEQ_1:def 3;
then
A8: rng f = Seg(k + 1) by FUNCT_2:def 3;
A9: now
let n;
assume n in dom f;
then f.n in Seg(k + 1) by A8,FUNCT_1:def 3;
hence f.n is Element of NAT;
end;
A10: rng H2 c= D by FINSEQ_1:def 4;
A11: dom f = Seg(k + 1) by A7,FUNCT_2:def 1;
A12: k + 1 in Seg(k + 1) by FINSEQ_1:4;
then
A13: f.(k + 1) in Seg(k + 1) by A11,A8,FUNCT_1:def 3;
then reconsider n = f.(k + 1) as Element of NAT;
A14: dom H2 = Seg(k + 1) by A5,A6,FINSEQ_1:def 3;
then H2.(k + 1) in rng H2 by A12,FUNCT_1:def 3;
then reconsider d = H2.(k + 1) as Element of D by A10;
A15: n <= k + 1 by A13,FINSEQ_1:1;
then consider m2 being Nat such that
A16: n + m2 = k + 1 by NAT_1:10;
defpred P[Nat,object] means $2 = H1.(n + $1);
1 <= n by A13,FINSEQ_1:1;
then consider m1 being Nat such that
A17: 1 + m1 = n by NAT_1:10;
reconsider m1, m2 as Element of NAT by ORDINAL1:def 12;
A18: for j be Nat st j in Seg m2 ex x being object st P[j,x];
consider q2 being FinSequence such that
A19: dom q2 = Seg m2 and
A20: for k be Nat st k in Seg m2 holds P[k,q2.k] from FINSEQ_1:sch 1
(A18);
rng q2 c= D
proof
let x be object;
assume x in rng q2;
then consider y being object such that
A21: y in findom q2 and
A22: x = q2.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A21,SETWISEO:9;
1 <= y by A19,A21,FINSEQ_1:1;
then
A23: 1 <= n + y by NAT_1:12;
y <= m2 by A19,A21,FINSEQ_1:1;
then n + y <= len H1 by A5,A16,XREAL_1:7;
then n + y in Seg(len H1) by A23,FINSEQ_1:1;
then n + y in dom H1 by FINSEQ_1:def 3;
then
A24: H1.(n + y) in rng H1 by FUNCT_1:def 3;
rng H1 c= D by FINSEQ_1:def 4;
then reconsider xx = H1.(n + y) as Element of D by A24;
xx in D;
hence thesis by A19,A20,A21,A22;
end;
then reconsider q2 as FinSequence of D by FINSEQ_1:def 4;
reconsider q1 = H1 | (Seg m1) as FinSequence of D by FINSEQ_1:18;
defpred P[Nat,object] means
(f.$1 in dom q1 implies $2 = f.$1) & (not f.$1
in dom q1 implies for l st l = f.$1 holds $2 = l - 1);
A25: k <= k + 1 by NAT_1:12;
then
A26: Seg k c= Seg(k + 1) by FINSEQ_1:5;
A27: for i be Nat st i in Seg k ex y being object st P[i,y]
proof
let i be Nat;
assume
A28: i in Seg k;
now
f.i in Seg(k + 1) by A11,A8,A26,A28,FUNCT_1:def 3;
then reconsider j = f.i as Element of NAT;
assume
A29: not f.i in dom q1;
take y = j - 1;
thus f.i in dom q1 implies y = f.i by A29;
assume not f.i in dom q1;
let t be Nat;
assume t = f.i;
hence y = t - 1;
end;
hence thesis;
end;
consider gg being FinSequence such that
A30: dom gg = Seg k and
A31: for i be Nat st i in Seg k holds P[i,gg.i] from FINSEQ_1:sch 1(
A27);
A32: dom p = Seg k by A5,A6,A25,FINSEQ_1:17;
m1 <= n by A17,NAT_1:11;
then
A33: m1 <= k + 1 by A15,XXREAL_0:2;
then
A34: dom q1 = Seg m1 by A5,FINSEQ_1:17;
A35: now
let i,l;
assume that
A36: l = f.i and
A37: not f.i in dom q1 and
A38: i in dom gg;
A39: l < 1 or m1 < l by A34,A36,A37,FINSEQ_1:1;
A40: now
assume m1 + 1 = l;
then k + 1 = i by A12,A11,A17,A26,A30,A36,A38,FUNCT_1:def 4;
then k + 1 <= k + 0 by A30,A38,FINSEQ_1:1;
hence contradiction by XREAL_1:6;
end;
f.i in rng f by A11,A26,A30,A38,FUNCT_1:def 3;
then m1 + 1 <= l by A8,A36,A39,FINSEQ_1:1,NAT_1:13;
then m1 + 1 < l by A40,XXREAL_0:1;
then m1 + 1 + 1 <= l by NAT_1:13;
hence m1 + 2 <= l;
end;
1 + k = 1 + (m1 + m2) by A17,A16;
then
A41: m1 <= k by NAT_1:11;
A42: rng gg c= dom p
proof
let y be object;
assume y in rng gg;
then consider x being object such that
A43: x in findom gg and
A44: gg.x = y by FUNCT_1:def 3;
reconsider x as Element of NAT by A43,SETWISEO:9;
now
per cases;
suppose
A45: f.x in dom q1;
A46: dom q1 c= dom p by A41,A34,A32,FINSEQ_1:5;
f.x = gg.x by A30,A31,A43,A45;
hence thesis by A44,A45,A46;
end;
suppose
A47: not f.x in dom q1;
reconsider j = f.x as Element of NAT by A11,A26,A9,A30,A43;
A48: f.x in Seg(k + 1) by A11,A8,A26,A30,A43,FUNCT_1:def 3;
j < 1 or m1 < j by A34,A47,FINSEQ_1:1;
then reconsider l = j - 1 as Element of NAT by A48,FINSEQ_1:1
,NAT_1:20;
j <= k + 1 by A48,FINSEQ_1:1;
then
A49: l <= (k + 1) - 1 by XREAL_1:9;
m1 + 2 <= j by A35,A43,A47;
then
A50: m1 + 2 - 1 <= l by XREAL_1:9;
1 <= m1 + 1 by NAT_1:12;
then
A51: 1 <= l by A50,XXREAL_0:2;
gg.x = j - 1 by A30,A31,A43,A47;
hence thesis by A32,A44,A51,A49,FINSEQ_1:1;
end;
end;
hence thesis;
end;
A52: len q1 = m1 by A5,A33,FINSEQ_1:17;
A53: now
let j be Nat;
assume
A54: j in dom q2;
len(q1 ^ <* d *>) = m1 + len<* d *> by A52,FINSEQ_1:22
.= n by A17,FINSEQ_1:39;
hence H1.(len(q1 ^ <* d *>) + j) = q2.j by A19,A20,A54;
end;
set q = q1 ^ q2;
A55: len q2 = m2 by A19,FINSEQ_1:def 3;
then
A56: len q = m1 + m2 by A52,FINSEQ_1:22;
then
A57: dom q = Seg k by A17,A16,FINSEQ_1:def 3;
then reconsider gg as Function of dom q, dom q by A32,A30,A42,FUNCT_2:2;
A58: len p = k by A5,A6,A25,FINSEQ_1:17;
A59: rng gg = dom q
proof
thus rng gg c= dom q by A17,A16,A56,A32,A42,FINSEQ_1:def 3;
let y be object;
assume
A60: y in dom q;
then reconsider j = y as Element of NAT;
consider x being object such that
A61: x in dom f and
A62: f.x = y by A8,A26,A57,A60,FUNCT_1:def 3;
reconsider x as Element of NAT by A11,A61;
now
per cases;
suppose
A63: x in dom gg;
now
per cases;
suppose
f.x in dom q1;
then gg.x = f.x by A30,A31,A63;
hence thesis by A62,A63,FUNCT_1:def 3;
end;
suppose
A64: not f.x in dom q1;
j <= k by A57,A60,FINSEQ_1:1;
then 1 <= j + 1 & j + 1 <= k + 1 by NAT_1:12,XREAL_1:7;
then j + 1 in rng f by A8,FINSEQ_1:1;
then consider x1 being object such that
A65: x1 in dom f and
A66: f.x1 = j + 1 by FUNCT_1:def 3;
A67: now
assume not x1 in dom gg;
then x1 in Seg(k + 1) \ Seg k by A7,A30,A65,XBOOLE_0:def 5;
then x1 in {k + 1} by FINSEQ_3:15;
then
A68: j + 1 = m1 +1 by A17,A66,TARSKI:def 1;
1 <= j by A57,A60,FINSEQ_1:1;
hence contradiction by A34,A62,A64,A68,FINSEQ_1:1;
end;
j < 1 or m1 < j by A34,A62,A64,FINSEQ_1:1;
then not j + 1 <= m1 by A57,A60,FINSEQ_1:1,NAT_1:13;
then not f.x1 in dom q1 by A34,A66,FINSEQ_1:1;
then gg.x1 = j + 1 - 1 by A30,A31,A66,A67
.= y;
hence thesis by A67,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
suppose
A69: not x in dom gg;
j <= k by A57,A60,FINSEQ_1:1;
then 1 <= j + 1 & j + 1 <= k + 1 by NAT_1:12,XREAL_1:7;
then j + 1 in rng f by A8,FINSEQ_1:1;
then consider x1 being object such that
A70: x1 in dom f and
A71: f.x1 = j + 1 by FUNCT_1:def 3;
x in Seg(k + 1) \ Seg k by A7,A30,A61,A69,XBOOLE_0:def 5;
then x in {k + 1} by FINSEQ_3:15;
then
A72: x = k + 1 by TARSKI:def 1;
A73: now
assume not x1 in dom gg;
then x1 in Seg(k + 1) \ Seg k by A7,A30,A70,XBOOLE_0:def 5;
then x1 in {k + 1} by FINSEQ_3:15;
then j + 1 = j + 0 by A62,A72,A71,TARSKI:def 1;
hence contradiction;
end;
m1 <= j by A17,A62,A72,XREAL_1:29;
then not j + 1 <= m1 by NAT_1:13;
then not f.x1 in dom q1 by A34,A71,FINSEQ_1:1;
then gg.x1 = j + 1 - 1 by A30,A31,A71,A73
.= y;
hence thesis by A73,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
assume
A74: for i st i in dom H2 holds H2.i = H1.(f.i);
then
A75: H2.(k + 1) = H1.(f.(k + 1)) by A14,FINSEQ_1:4;
A76: now
let j be Nat;
assume
A77: j in dom(q1 ^ <* d *>);
A78: now
assume j in Seg m1;
then
A79: j in dom q1 by A5,A33,FINSEQ_1:17;
then q1.j = H1.j by FUNCT_1:47;
hence H1.j = (q1 ^ <* d *>).j by A79,FINSEQ_1:def 7;
end;
A80: now
1 in Seg 1 & len<* d *> = 1 by FINSEQ_1:1,39;
then 1 in dom <* d *> by FINSEQ_1:def 3;
then
A81: (q1 ^ <* d *>).(len q1 + 1) = <* d *>.1 by FINSEQ_1:def 7;
assume j in {n};
then j = n by TARSKI:def 1;
hence (q1 ^ <* d *>).j = H1.j by A75,A17,A52,A81;
end;
len(q1 ^ <* d *>) = m1 + len <* d *> by A52,FINSEQ_1:22
.= m1 + 1 by FINSEQ_1:40;
then j in Seg(m1 + 1) by A77,FINSEQ_1:def 3;
then j in Seg m1 \/ {n} by A17,FINSEQ_1:9;
hence H1.j = (q1 ^ <* d *>).j by A78,A80,XBOOLE_0:def 3;
end;
gg is one-to-one
proof
let y1,y2 be object;
assume that
A82: y1 in dom gg and
A83: y2 in dom gg and
A84: gg.y1 = gg.y2;
reconsider j1 = y1, j2 = y2 as Element of NAT by A30,A82,A83;
A85: f.y2 in Seg(k + 1) by A11,A8,A26,A30,A83,FUNCT_1:def 3;
A86: f.y1 in Seg(k + 1) by A11,A8,A26,A30,A82,FUNCT_1:def 3;
then reconsider a = f.y1, b = f.y2 as Element of NAT by A85;
now
per cases;
suppose
f.y1 in dom q1 & f.y2 in dom q1;
then gg.j1 = f.y1 & gg.j2 = f.y2 by A30,A31,A82,A83;
hence thesis by A11,A26,A30,A82,A83,A84,FUNCT_1:def 4;
end;
suppose
A87: f.y1 in dom q1 & not f.y2 in dom q1;
then
A88: a <= m1 by A34,FINSEQ_1:1;
gg.j1 = a & gg.j2 = b - 1 by A30,A31,A82,A83,A87;
then
A89: (b - 1) + 1 <= m1 + 1 by A84,A88,XREAL_1:6;
1 <= b by A85,FINSEQ_1:1;
then
A90: b in Seg(m1 + 1) by A89,FINSEQ_1:1;
not b in Seg m1 by A5,A33,A87,FINSEQ_1:17;
then b in Seg(m1 + 1) \ Seg m1 by A90,XBOOLE_0:def 5;
then b in {m1 + 1} by FINSEQ_3:15;
then b = m1 + 1 by TARSKI:def 1;
then y2 = k + 1 by A12,A11,A17,A26,A30,A83,FUNCT_1:def 4;
hence thesis by A30,A83,FINSEQ_3:8;
end;
suppose
A91: not f.y1 in dom q1 & f.y2 in dom q1;
then
A92: b <= m1 by A34,FINSEQ_1:1;
gg.j1 = a - 1 & gg.j2 = b by A30,A31,A82,A83,A91;
then
A93: (a - 1) + 1 <= m1 + 1 by A84,A92,XREAL_1:6;
1 <= a by A86,FINSEQ_1:1;
then
A94: a in Seg(m1 + 1) by A93,FINSEQ_1:1;
not a in Seg m1 by A5,A33,A91,FINSEQ_1:17;
then a in Seg(m1 + 1) \ Seg m1 by A94,XBOOLE_0:def 5;
then a in {m1 + 1} by FINSEQ_3:15;
then a = m1 + 1 by TARSKI:def 1;
then y1 = k + 1 by A12,A11,A17,A26,A30,A82,FUNCT_1:def 4;
hence thesis by A30,A82,FINSEQ_3:8;
end;
suppose
A95: not f.y1 in dom q1 & not f.y2 in dom q1;
then gg.j2 = b - 1 by A30,A31,A83;
then
A96: gg.y2 = b + (- 1);
gg.j1 = a - 1 by A30,A31,A82,A95;
then gg.j1 = a + (- 1);
then a = b by A84,A96,XCMPLX_1:2;
hence thesis by A11,A26,A30,A82,A83,FUNCT_1:def 4;
end;
end;
hence thesis;
end;
then reconsider gg as Permutation of dom q by A59,FUNCT_2:57;
len(q1 ^ <* d *>) + len q2 = len q1 + len<* d *> + m2 by A55,FINSEQ_1:22
.= k + 1 by A17,A16,A52,FINSEQ_1:40;
then dom H1 = Seg(len(q1 ^ <* d *>) + len q2) by A5,FINSEQ_1:def 3;
then
A97: H1 = q1 ^ <* d *> ^ q2 by A76,A53,FINSEQ_1:def 7;
A98: now
let i;
assume
A99: i in dom p;
then f.i in rng f by A11,A26,A32,FUNCT_1:def 3;
then reconsider j = f.i as Element of NAT by A8;
now
per cases;
suppose
A100: f.i in dom q1;
then
A101: f.i = gg.i & H1.(j) = q1.(j) by A32,A31,A99,FUNCT_1:47;
H2.i = p.i & H2.i = H1.(f.i) by A74,A14,A26,A32,A99,FUNCT_1:47;
hence p.i = q.(gg.i) by A100,A101,FINSEQ_1:def 7;
end;
suppose
A102: not f.i in dom q1;
then m1 + 2 <= j by A32,A30,A35,A99;
then
A103: m1 + 2 - 1 <= j - 1 by XREAL_1:9;
m1 < m1 + 1 by XREAL_1:29;
then
A104: m1 < j - 1 by A103,XXREAL_0:2;
then m1 < j by XREAL_1:146,XXREAL_0:2;
then reconsider j1 = j - 1 as Element of NAT by NAT_1:20;
A105: not j1 in dom q1 by A34,A104,FINSEQ_1:1;
A106: gg.i = j - 1 by A32,A31,A99,A102;
then j - 1 in dom q by A32,A30,A59,A99,FUNCT_1:def 3;
then consider a being Nat such that
A107: a in dom q2 and
A108: j1 = len q1 + a by A105,FINSEQ_1:25;
A109: len<* d *> = 1 by FINSEQ_1:39;
A110: H2.i = p.i & H2.i = H1.(f.i) by A74,A14,A26,A32,A99,FUNCT_1:47;
A111: H1 = q1 ^ (<* d *> ^ q2) by A97,FINSEQ_1:32;
j in dom H1 by A7,A11,A8,A26,A32,A99,FUNCT_1:def 3;
then consider b being Nat such that
A112: b in dom(<* d *> ^ q2) and
A113: j = len q1 + b by A102,A111,FINSEQ_1:25;
A114: H1.j = (<* d *> ^ q2).b by A111,A112,A113,FINSEQ_1:def 7;
A115: b = 1 + a by A108,A113;
q.(j - 1) = q2.a by A107,A108,FINSEQ_1:def 7;
hence p.i = q.(gg.i) by A106,A110,A107,A114,A115,A109,
FINSEQ_1:def 7;
end;
end;
hence p.i = q.(gg.i);
end;
now
per cases;
suppose
A116: len p <> 0;
A117: H2 = p ^ <* d *> by A5,A6,FINSEQ_3:55;
g "**" p = g "**" q by A4,A17,A16,A58,A56,A98,A116,NAT_1:14;
then
A118: g "**" H2 = g.(g "**" q,d) by A116,A117,Th4,NAT_1:14;
now
per cases;
suppose
A119: len q1 <> 0 & len q2 <> 0;
len(<* d *> ^ q2) = len<* d *> + len q2 & len<* d *> = 1
by FINSEQ_1:22,40;
then
A120: len(<* d *> ^ q2) >= 1 by NAT_1:12;
A121: len q1 >= 1 by A119,NAT_1:14;
len q2 >= 1 by A119,NAT_1:14;
then g "**" H2 = g.(g.(g "**" q1,g "**" q2),d) by A1,A118,A121
,Th5
.= g.(g "**" q1,g.(g "**" q2,d)) by A1,BINOP_1:def 3
.= g.(g "**" q1,g.(d,g "**" q2)) by A2,BINOP_1:def 2
.= g.(g "**" q1,g "**" (<* d *> ^ q2)) by A1,A119,Th6,NAT_1:14
.= g "**" (q1 ^ (<* d *> ^ q2)) by A1,A121,A120,Th5
.= g "**" H1 by A97,FINSEQ_1:32;
hence thesis;
end;
suppose
len q1 = 0 & len q2 <> 0;
then
A122: q1 = {};
then
A123: H1 = <* d *> ^ q2 by A97,FINSEQ_1:34
.= <* d *> ^ q by A122,FINSEQ_1:34;
g "**" H2 = g.(d,g "**" q) by A2,A118,BINOP_1:def 2
.= g "**" (<* d *> ^ q) by A1,A17,A16,A58,A56,A116,Th6,NAT_1:14
;
hence thesis by A123;
end;
suppose
len q1 <> 0 & len q2 = 0;
then
A124: q2 = {};
then H1 = q1 ^ <* d *> by A97,FINSEQ_1:34
.= q ^ <* d *> by A124,FINSEQ_1:34;
hence thesis by A17,A16,A58,A56,A116,A118,Th4,NAT_1:14;
end;
suppose
len q1 = 0 & len q2 = 0;
then len q = 0 + 0 by FINSEQ_1:22;
hence thesis by A6,A17,A16,A56,A116,FINSEQ_1:17;
end;
end;
hence thesis;
end;
suppose
A125: len p = 0;
then dom H1 = {1} by A5,A58,FINSEQ_1:2,def 3;
then
A126: dom f = {1} & rng f = {1} by FUNCT_2:def 1,def 3;
1 in {1} by TARSKI:def 1;
then f.1 in {1} by A126,FUNCT_1:def 3;
then H1.1 = H2.1 by A75,A58,A125,TARSKI:def 1;
then H1 = <* d *> by A5,A58,A125,FINSEQ_1:40;
hence thesis by A5,A6,A58,A125,FINSEQ_1:40;
end;
end;
hence thesis;
end;
end;
let f be Permutation of dom F;
A127: P[0];
for k holds P[k] from NAT_1:sch 2(A127,A3);
hence thesis;
end;
Lm8: g is having_a_unity & len F = 0 & G = F * P implies g "**" F = g "**" G
proof
assume that
A1: g is having_a_unity and
A2: len F = 0;
assume
A3: G = F * P;
F = {} by A2;
then G = {} by A3,RELAT_1:39;
then
A4: len G = 0;
thus g "**" F = the_unity_wrt g by A1,A2,Def1
.= g "**" G by A1,A4,Def1;
end;
theorem Th7:
g is commutative associative & (g is having_a_unity or len F >= 1
) & G = F * P implies g "**" F = g "**" G
proof
assume that
A1: g is commutative associative and
A2: g is having_a_unity or len F >= 1;
assume
A3: G = F * P;
now
per cases;
suppose
len F = 0;
hence thesis by A2,A3,Lm8;
end;
suppose
A4: len F <> 0;
len F = len G & for i st i in dom G holds G.i = F.(P.i) by A3,FINSEQ_2:44
,FUNCT_1:12;
hence thesis by A1,A4,Lm7,NAT_1:14;
end;
end;
hence thesis;
end;
Lm9: g is associative commutative & F is one-to-one & G is one-to-one & rng F
= rng G & len F >= 1 implies g "**" F = g "**" G
proof
assume that
A1: g is associative commutative and
A2: F is one-to-one and
A3: G is one-to-one and
A4: rng F = rng G and
A5: len F >= 1;
A6: len F = len G by A2,A3,A4,FINSEQ_1:48;
set P = F" * G;
A7: dom(F") = rng F by A2,FUNCT_1:33;
then
A8: dom P = dom G by A4,RELAT_1:27
.= Seg len F by A6,FINSEQ_1:def 3
.= dom F by FINSEQ_1:def 3;
rng(F") = dom F by A2,FUNCT_1:33;
then
A9: rng P c= dom F by RELAT_1:26;
dom F = Seg len F by FINSEQ_1:def 3;
then reconsider P as Function of dom F, dom F by A5,A8,A9,FUNCT_2:def 1
,RELSET_1:4;
rng P = rng(F") by A4,A7,RELAT_1:28
.= dom F by A2,FUNCT_1:33;
then reconsider P as Permutation of dom F by A2,A3,FUNCT_2:57;
F * P = (F * F") * G by RELAT_1:36
.= id(rng G) * G by A2,A4,FUNCT_1:39
.= G by RELAT_1:54;
hence thesis by A1,A5,Th7;
end;
Lm10: len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one &
rng F = rng G implies g "**" F = g "**" G
proof
assume that
A1: len F = 0 & g is having_a_unity and
A2: F is one-to-one & G is one-to-one & rng F = rng G;
len G = len F & g "**" F = the_unity_wrt g by A1,A2,Def1,FINSEQ_1:48;
hence thesis by A1,Def1;
end;
theorem
(g is having_a_unity or len F >= 1) & g is associative commutative & F
is one-to-one & G is one-to-one & rng F = rng G implies g "**" F = g "**" G
proof
len F >= 1 or len F = 0 by NAT_1:14;
hence thesis by Lm9,Lm10;
end;
Lm11: len F = 1 implies g "**" F = F.1
proof
assume
A1: len F = 1;
then F = <* F.1 *> by FINSEQ_1:40
.= <* F/.1 *> by A1,FINSEQ_4:15;
hence g "**" F = F/.1 by Lm4
.= F.1 by A1,FINSEQ_4:15;
end;
Lm12: g is associative & g is commutative & len F >= 1 & len F = len G & len F
= len H & (for k being Nat st k in dom F holds H.k = g.(F.k,G.k))
implies g "**" H = g.(g"**" F,g "**" G)
proof
assume that
A1: g is associative and
A2: g is commutative;
defpred P[Nat] means
for F,G,H st len F >= 1 & len F = $1 & len F = len G & len F = len H &
(for n being Nat st n in dom F holds H.n = g.(F.n,G.n))
holds g "**" H = g.(g "**" F,g "**" G);
A3: now
let k be Nat;
assume
A4: P[k];
thus P[k+1]
proof
let F,G,H;
assume that
len F >= 1 and
A5: len F = k + 1 and
A6: len F = len G and
A7: len F = len H and
A8: for k being Nat st k in dom F holds H.k = g.(F.k,G.k);
reconsider f = F | Seg k,gg = G | Seg k,h = H | Seg k as FinSequence of
D by FINSEQ_1:18;
A9: len h = k by A5,A7,FINSEQ_3:53;
A10: len f = k by A5,FINSEQ_3:53;
A11: len gg = k by A5,A6,FINSEQ_3:53;
A12: now
k <= k + 1 by NAT_1:12;
then Seg len f c= Seg len F by A5,A10,FINSEQ_1:5;
then Seg len f c= dom F by FINSEQ_1:def 3;
then
A13: dom f c= dom F by FINSEQ_1:def 3;
let i be Nat;
assume
A14: i in dom f;
then i in Seg len gg by A10,A11,FINSEQ_1:def 3;
then i in dom gg by FINSEQ_1:def 3;
then
A15: G.i = gg.i by FUNCT_1:47;
i in Seg len h by A10,A9,A14,FINSEQ_1:def 3;
then i in dom h by FINSEQ_1:def 3;
then
A16: H.i = h.i by FUNCT_1:47;
F.i = f.i by A14,FUNCT_1:47;
hence h.i = g.(f.i,gg.i) by A8,A14,A15,A16,A13;
end;
now
per cases by NAT_1:14;
suppose
A17: len f >= 1;
A18: rng H c= D by FINSEQ_1:def 4;
A19: rng F c= D & rng G c= D by FINSEQ_1:def 4;
A20: k + 1 in Seg(k + 1) by FINSEQ_1:4;
then k + 1 in dom G by A5,A6,FINSEQ_1:def 3;
then
A21: (G.(k + 1)) in rng G by FUNCT_1:def 3;
k + 1 in dom H by A5,A7,A20,FINSEQ_1:def 3;
then
A22: (H.(k + 1)) in rng H by FUNCT_1:def 3;
A23: k + 1 in dom F by A5,A20,FINSEQ_1:def 3;
then (F.(k + 1)) in rng F by FUNCT_1:def 3;
then reconsider
d = F.(k + 1),d1 = G.(k + 1),d2 = H.(k + 1) as Element of
D by A21,A22,A19,A18;
A24: d2 = g.(F.(k + 1),G.(k + 1)) by A8,A23;
F = f ^ <* d *> by A5,FINSEQ_3:55;
then
A25: g "**" F = g.(g "**" f,d) by A17,Th4;
G = gg ^ <* d1 *> by A5,A6,FINSEQ_3:55;
then
A26: g "**" G = g.(g "**" gg,d1) by A10,A11,A17,Th4;
A27: H = h ^ <* d2 *> by A5,A7,FINSEQ_3:55;
g "**" h = g.(g "**" f,g "**" gg) by A4,A10,A11,A9,A12,A17;
hence g "**" H = g.(g.(g "**" f,g "**" gg),g.(d,d1)) by A10,A9,A17
,A27,A24,Th4
.= g.(g.(g.(g "**" f,g "**" gg),d),d1) by A1,BINOP_1:def 3
.= g.(g.(g "**" f,g.(g "**" gg,d)),d1) by A1,BINOP_1:def 3
.= g.(g.(g "**" f,g.(d,g "**" gg)),d1) by A2,BINOP_1:def 2
.= g.(g.(g "**" F,g "**" gg),d1) by A1,A25,BINOP_1:def 3
.= g.(g "**" F,g "**" G) by A1,A26,BINOP_1:def 3;
end;
suppose
A28: len f = 0;
then
A29: g "**" G = G.1 & 1 in dom F by A5,A6,A10,Lm11,FINSEQ_3:25;
g "**" H = H.1 & g "**" F = F.1 by A5,A7,A10,A28,Lm11;
hence thesis by A8,A29;
end;
end;
hence thesis;
end;
end;
assume
A30: len F >= 1 & len F = len G & len F = len H;
A31: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A31,A3);
hence thesis by A30;
end;
Lm13: g is having_a_unity & len F = 0 & len F = len G & len F = len H implies
g "**" F = g.(g "**" G,g "**" H)
proof
assume that
A1: g is having_a_unity and
A2: len F = 0 and
A3: len F = len G and
A4: len F = len H;
thus g "**" F = the_unity_wrt g by A1,A2,Def1
.= g.(the_unity_wrt g,the_unity_wrt g) by A1,SETWISEO:15
.= g.(g "**" G,the_unity_wrt g) by A1,A2,A3,Def1
.= g.(g "**" G,g "**" H) by A1,A2,A4,Def1;
end;
theorem
g is associative commutative & (g is having_a_unity or len F >= 1) &
len F = len G & len F = len H &
(for k being Nat st k in dom F holds F.k = g.(G.k,H.k))
implies g "**" F = g.(g "**" G,g "**" H)
proof
A1: dom F = Seg len F & dom G = Seg len G by FINSEQ_1:def 3;
A2: len F = 0 or len F >= 1 by NAT_1:14;
assume g is associative commutative &( g is having_a_unity or len F >= 1);
hence thesis by A1,A2,Lm12,Lm13;
end;
theorem
g is having_a_unity implies g "**" <*>D = the_unity_wrt g by Lm3;
theorem
g "**" <* d *> = d by Lm4;
theorem Th12:
g "**" <* d1,d2 *> = g.(d1,d2)
proof
A1: len<* d1 *> = 1 by FINSEQ_1:39;
thus g "**" <* d1,d2 *> = g "**" (<* d1 *> ^ <* d2 *>) by FINSEQ_1:def 9
.= g.(g "**" <* d1 *>,d2) by A1,Th4
.= g.(d1,d2) by Lm4;
end;
theorem
g is commutative implies g "**" <* d1,d2 *> = g "**" <* d2,d1 *>
proof
assume
A1: g is commutative;
thus g "**" <* d1,d2 *> = g.(d1,d2) by Th12
.= g.(d2,d1) by A1,BINOP_1:def 2
.= g "**" <* d2,d1 *> by Th12;
end;
theorem Th14:
g "**" <* d1,d2,d3 *> = g.(g.(d1,d2),d3)
proof
A1: len<* d1,d2 *> = 2 by FINSEQ_1:44;
thus g "**" <* d1,d2,d3 *> = g "**" (<* d1,d2 *> ^ <* d3 *>) by FINSEQ_1:43
.= g.(g "**" <* d1,d2 *>,d3) by A1,Th4
.= g.(g.(d1,d2),d3) by Th12;
end;
theorem
g is commutative implies g "**" <* d1,d2,d3 *> = g "**" <* d2,d1,d3 *>
proof
assume
A1: g is commutative;
thus g "**" <* d1,d2,d3 *> = g.(g.(d1,d2),d3) by Th14
.= g.(g.(d2,d1),d3) by A1,BINOP_1:def 2
.= g "**" <* d2,d1,d3 *> by Th14;
end;
theorem Th16:
g "**" (1 |-> d) = d
proof
thus g "**" (1 |-> d) = g "**" <* d *> by FINSEQ_2:59
.= d by Lm4;
end;
theorem
g "**" (2 |-> d) = g.(d,d)
proof
thus g "**" (2 |-> d) = g "**" <* d,d *> by FINSEQ_2:61
.= g.(d,d) by Th12;
end;
theorem Th18:
g is associative & (g is having_a_unity or k <> 0 & l <> 0)
implies g "**" ((k + l) |-> d) = g.(g "**" (k |-> d),g "**" (l |-> d))
proof
A1: k <> 0 & l <> 0 implies len(k |-> d) >= 1 & len(l |-> d) >= 1 by NAT_1:14;
(k + l) |-> d = (k |-> d) ^ (l |-> d) by FINSEQ_2:123;
hence thesis by A1,Th5;
end;
theorem
g is associative & (g is having_a_unity or k <> 0 & l <> 0) implies g
"**" (k * l |-> d) = g "**" (l |-> (g "**" (k |-> d)))
proof
defpred P[Nat] means for g,k,d st g is associative & (g is
having_a_unity or k <> 0 & $1 <> 0) holds g "**" (k * $1 |-> d) = g "**" ($1
|-> (g "**" (k |-> d)));
A1: for l st P[l] holds P[l + 1]
proof
let l;
assume
A2: P[l];
let g,k,d;
assume that
A3: g is associative and
A4: g is having_a_unity or k <> 0 & l + 1 <> 0;
now
per cases;
suppose
l = 0;
hence thesis by Th16;
end;
suppose
A5: l <> 0;
then
A6: k <> 0 implies k * l <> 0 by XCMPLX_1:6;
g "**" (k * (l + 1) |-> d) = g "**" ((k * l + k * 1) |-> d)
.= g.(g "**" (k * l |-> d),g "**" (k |-> d)) by A3,A4,A6,Th18
.= g.(g "**" (l |-> (g "**" (k |-> d))),g "**" (k |-> d)) by A2,A3,A4
,A5
.= g.(g "**" (l |-> (g "**" (k |-> d))),g "**" (1 |-> (g "**" (k
|-> d)))) by Th16;
hence thesis by A3,A5,Th18;
end;
end;
hence thesis;
end;
A7: P[0];
for l holds P[l] from NAT_1:sch 2(A7,A1);
hence thesis;
end;
theorem
len F = 1 implies g "**" F = F.1 by Lm11;
theorem
len F = 2 implies g "**" F = g.(F.1,F.2)
proof
assume
A1: len F = 2;
then F = <* F.1,F.2 *> by FINSEQ_1:44
.= <* F/.1,F.2 *> by A1,FINSEQ_4:15
.= <* F/.1,F/.2 *> by A1,FINSEQ_4:15;
hence g "**" F = g.(F/.1,F/.2) by Th12
.= g.(F.1,F/.2) by A1,FINSEQ_4:15
.= g.(F.1,F.2) by A1,FINSEQ_4:15;
end;