### The Mizar article:

### Binary Operations Applied to Finite Sequences

**by****Czeslaw Bylinski**

- Received May 4, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: FINSEQOP
- [ MML identifier index ]

environ vocabulary FUNCT_1, PARTFUN1, BOOLE, RELAT_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, BINOP_1, SETWISEO, FINSEQOP; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3, FUNCOP_1, FINSEQ_2, SETWISEO; constructors NAT_1, BINOP_1, FUNCT_3, FUNCOP_1, FINSEQ_2, SETWISEO, RELAT_2, PARTFUN1, XBOOLE_0; clusters SUBSET_1, RELAT_1, FUNCT_1, FINSEQ_2, RELSET_1, FUNCOP_1, ARYTM_3, ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0; requirements NUMERALS, BOOLE, SUBSET; definitions BINOP_1; theorems ZFMISC_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSEQ_1, BINOP_1, SETWISEO, FINSEQ_2, FUNCT_3, FUNCT_4, RELAT_1, XBOOLE_0; schemes NAT_1, FINSEQ_2; begin reserve x,y for set; reserve C,C',D,D',E for non empty set; reserve c for Element of C; reserve c' for Element of C'; reserve d,d1,d2,d3,d4,e for Element of D; reserve d' for Element of D'; :: Auxiliary theorems theorem Th1: for f being Function holds <:{},f:> = {} & <:f,{}:> = {} proof let f be Function; dom <:{},f:> = dom {} /\ dom f & dom <:f,{}:> = dom f /\ dom {} by FUNCT_3: def 8; hence thesis by RELAT_1:64; end; theorem for f being Function holds [:{},f:] = {} & [:f,{}:] = {} proof let f be Function; dom [:{},f:] = [:dom {},dom f:] & dom [:f,{}:] = [:dom f,dom {}:] by FUNCT_3:def 9; then dom [:{},f:] = {} & dom [:f,{}:] = {} by ZFMISC_1:113; hence thesis by RELAT_1:64; end; canceled; theorem Th4: for F,f being Function holds F.:({},f) = {} & F.:(f,{}) = {} proof let F,f be Function; F.:({},f) = F*<:{},f:> & F.:(f,{}) = F*<:f,{}:> by FUNCOP_1:def 3; then F.:({},f) = F*{} & F.:(f,{}) = F*{} by Th1; hence thesis; end; theorem for F being Function holds F[:]({},x) = {} proof let F be Function; F[:]({},x) = F.:({}, dom {} --> x) by FUNCOP_1:34; hence thesis by Th4; end; theorem for F being Function holds F[;](x,{}) = {} proof let F be Function; F[;](x,{}) = F.:(dom {} --> x, {}) by FUNCOP_1:41; hence thesis by Th4; end; theorem Th7: for X being set, x1,x2 being set holds <:X-->x1,X-->x2:> = X -->[x1,x2] proof let X be set, x1,x2 be set; set f = X-->x1, g = X-->x2; set fg = <:f,g:>; now per cases; suppose A1: X = {}; then f = {} by FUNCT_4:3; then fg = {} by Th1; hence thesis by A1,FUNCT_4:3; suppose A2: X <> {}; consider x being Element of X; A3: dom f = X & dom g = X by FUNCOP_1:19; then A4: dom fg = X by FUNCT_3:70; f.x = x1 & g.x = x2 by A2,FUNCOP_1:13; then fg.x = [x1,x2] & rng f = {x1} & rng g = {x2} by A2,A3,FUNCOP_1:14,FUNCT_3:69; then [x1,x2] in rng fg & rng fg c= [:{x1},{x2}:] by A2,A4,FUNCT_1:def 5,FUNCT_3:71; then rng fg c= {[x1,x2]} & {[x1,x2]} c= rng fg by ZFMISC_1:35,37; then rng fg = {[x1,x2]} by XBOOLE_0:def 10; hence thesis by A4,FUNCOP_1:15; end; hence thesis; end; theorem Th8: for F being Function,X being set, x1,x2 being set st [x1,x2] in dom F holds F.:(X-->x1,X-->x2) = X -->(F.[x1,x2]) proof let F be Function, X be set, x1,x2 be set such that A1: [x1,x2] in dom F; set f = X-->x1, g = X-->x2; thus F.:(f,g) = F*<:f,g:> by FUNCOP_1:def 3 .= F*(X-->[x1,x2]) by Th7 .= X -->(F.[x1,x2]) by A1,FUNCOP_1:23; end; reserve i,j for Nat; reserve F for Function of [:D,D':],E; reserve p,q for FinSequence of D, p',q' for FinSequence of D'; definition let D,D',E,F,p,p'; redefine func F.:(p,p') -> FinSequence of E; coherence by FINSEQ_2:84; end; definition let D,D',E,F,p,d'; redefine func F[:](p,d') -> FinSequence of E; coherence by FINSEQ_2:97; end; definition let D,D',E,F,d,p'; redefine func F[;](d,p') -> FinSequence of E; coherence by FINSEQ_2:91; end; definition let D,i,d; redefine func i|-> d -> Element of i-tuples_on D; coherence by FINSEQ_2:132; end; reserve f,f' for Function of C,D, h for Function of D,E; definition let D,E be set, p be FinSequence of D, h be Function of D,E; redefine func h*p -> FinSequence of E; coherence by FINSEQ_2:36; end; theorem Th9: h*(p^<*d*>) = (h*p)^<*h.d*> proof set q = h*(p^<*d*>); set r = (h*p)^<*h.d*>; set i = len p + 1; A1: len q = len(p^<*d*>) by FINSEQ_2:37; A2: len(p^<*d*>) = i by FINSEQ_2:19; A3: len r = len(h*p)+1 by FINSEQ_2:19; A4: len(h*p) = len p by FINSEQ_2:37; now let j; assume A5: j in Seg i; then A6: j in dom q & j in dom r by A1,A2,A3,A4,FINSEQ_1:def 3; A7: Seg len p = dom p by FINSEQ_1:def 3; A8: Seg len(h*p) = dom(h*p) by FINSEQ_1:def 3; now per cases by A5,A7,FINSEQ_2:8; suppose A9: j in dom p; hence h.((p^<*d*>).j) = h.(p.j) by FINSEQ_1:def 7 .= (h*p).j by A4,A7,A8,A9,FUNCT_1:22 .= r.j by A4,A7,A8,A9,FINSEQ_1:def 7; suppose A10: j = i; hence h.((p^<*d*>).j) = h.d by FINSEQ_1:59 .= r.j by A4,A10,FINSEQ_1:59; end; hence q.j = r.j by A6,FUNCT_1:22; end; hence thesis by A1,A2,A3,A4,FINSEQ_2:10; end; theorem h*(p^q) = (h*p)^(h*q) proof defpred P[FinSequence of D] means h*(p^$1) = (h*p)^(h*$1); h*(p^<*>D) = h*p by FINSEQ_1:47 .= (h*p)^(h*(<*>D)) by FINSEQ_1:47; then A1: P[<*>D]; A2: for q,d st P[q] holds P[q^<*d*>] proof let q,d such that A3: h*(p^q) = (h*p)^(h*q); thus h*(p^(q^<*d*>)) = h*((p^q)^<*d*>) by FINSEQ_1:45 .= (h*(p^q))^<*h.d*> by Th9 .= (h*p)^((h*q)^<*h.d*>) by A3,FINSEQ_1:45 .= (h*p)^(h*(q^<*d*>)) by Th9; end; for q holds P[q] from IndSeqD(A1,A2); hence thesis; end; reserve T,T1,T2,T3 for Element of i-tuples_on D; reserve T' for Element of i-tuples_on D'; reserve S,S1 for Element of j-tuples_on D; reserve S',S1' for Element of j-tuples_on D'; Lm1: for T being Element of 0-tuples_on C holds f*T = <*>D proof let T be Element of 0-tuples_on C; T = <*>C by FINSEQ_2:113; hence thesis by FINSEQ_2:38; end; Lm2: for T being Element of 0-tuples_on D holds F.:(T,T') = <*>E proof let T be Element of 0-tuples_on D; T = <*>D by FINSEQ_2:113; hence thesis by FINSEQ_2:87; end; Lm3: for T' being Element of 0-tuples_on D' holds F[;](d,T') = <*>E proof let T' be Element of 0-tuples_on D'; T' = <*>D' by FINSEQ_2:113; hence thesis by FINSEQ_2:93; end; Lm4: for T being Element of 0-tuples_on D holds F[:](T,d') = <*>E proof let T be Element of 0-tuples_on D; T = <*>D by FINSEQ_2:113; hence thesis by FINSEQ_2:99; end; theorem Th11: F.:(T^<*d*>,T'^<*d'*>) = (F.:(T,T'))^<*F.(d,d')*> proof set p = T^<*d*>, q = T'^<*d'*>, pq = F.:(T,T'); set r = F.:(p,q), s = pq^<*F.(d,d')*>; A1: len T = i & len T' = i by FINSEQ_2:109; then len p = i+1 & len q = i+1 by FINSEQ_2:19; then A2: len r = i+1 by FINSEQ_2:86; A3: len pq = i by A1,FINSEQ_2:86; A4: len s = len pq + 1 by FINSEQ_2:19; now let j; assume A5: j in Seg(i+1); then A6: j in dom r by A2,FINSEQ_1:def 3; now per cases by A5,FINSEQ_2:8; suppose A7: j in Seg i; then A8: j in dom pq by A3,FINSEQ_1:def 3; A9: Seg len pq = dom pq by FINSEQ_1:def 3; Seg len T = dom T & Seg len T' = dom T' by FINSEQ_1:def 3; then p.j = T.j & q.j = T'.j by A1,A7,FINSEQ_1:def 7; hence F.(p.j,q.j) = pq.j by A8,FUNCOP_1:28 .= s.j by A3,A7,A9,FINSEQ_1:def 7; suppose A10: j = i+1; then p.j = d & q.j = d' by A1,FINSEQ_1:59; hence F.(p.j,q.j) = s.j by A3,A10,FINSEQ_1:59; end; hence r.j = s.j by A6,FUNCOP_1:28; end; hence thesis by A2,A3,A4,FINSEQ_2:10; end; theorem F.:(T^S,T'^S') = (F.:(T,T'))^(F.:(S,S')) proof defpred P[Nat] means for S being Element of $1-tuples_on D, S' being Element of $1-tuples_on D' holds F.:(T^S,T'^S') = (F.:(T,T'))^(F.:(S,S')); now let S be Element of 0-tuples_on D; let S' be Element of 0-tuples_on D'; S = <*>D by FINSEQ_2:113; then T^S = T & T'^S' = T' & F.:(S,S') = <*>E & <*>E = {} by FINSEQ_2:87,115; hence F.:(T^S,T'^S') = (F.:(T,T'))^(F.:(S,S')) by FINSEQ_1:47; end; then A1: P[0]; now let j such that A2: for S,S' holds F.:(T^S,T'^S') = (F.:(T,T'))^(F.:(S,S')); let S be Element of (j+1)-tuples_on D; let S' be Element of (j+1)-tuples_on D'; consider S1,d such that A3: S = S1^<*d*> by FINSEQ_2:137; consider S1',d' such that A4: S' = S1'^<*d'*> by FINSEQ_2:137; T^S1 is Element of (i+j)-tuples_on D & T^S = T^S1^<*d*> & T'^S1' is Element of (i+j)-tuples_on D' & T'^S' = T'^S1'^<*d'*> by A3,A4,FINSEQ_1:45,FINSEQ_2:127; hence F.:(T^S,T'^S') = (F.:(T^S1,T'^S1'))^<*F.(d,d')*> by Th11 .= (F.:(T,T'))^(F.:(S1,S1'))^<*F.(d,d')*> by A2 .= (F.:(T,T'))^((F.:(S1,S1'))^<*F.(d,d')*>) by FINSEQ_1:45 .= (F.:(T,T'))^(F.:(S,S')) by A3,A4,Th11; end; then A5: for j st P[j] holds P[j+1]; for j holds P[j] from Ind(A1,A5); hence thesis; end; theorem Th13: F[;](d,p'^<*d'*>) = (F[;](d,p'))^<*F.(d,d')*> proof set pd = p'^<*d'*>, q = F[;](d,p'); set r = F[;](d,pd), s = q^<*F.(d,d')*>; set i = len p'; A1: len pd = i + 1 by FINSEQ_2:19; A2: len q = i by FINSEQ_2:92; A3: len r = i + 1 by A1,FINSEQ_2:92; A4: len s = len q + 1 by FINSEQ_2:19; now let j; assume A5: j in Seg(i+1); then A6: j in dom r by A3,FINSEQ_1:def 3; now per cases by A5,FINSEQ_2:8; suppose A7: j in Seg i; then A8: j in dom q by A2,FINSEQ_1:def 3; A9: Seg len q = dom q by FINSEQ_1:def 3; Seg len p' = dom p' by FINSEQ_1:def 3; hence F.(d,pd.j) = F.(d,p'.j) by A7,FINSEQ_1:def 7 .= q.j by A8,FUNCOP_1:42 .= s.j by A2,A7,A9,FINSEQ_1:def 7; suppose A10: j = i+1; hence F.(d,pd.j) = F.(d,d') by FINSEQ_1:59 .= s.j by A2,A10,FINSEQ_1:59; end; hence r.j = s.j by A6,FUNCOP_1:42; end; hence thesis by A2,A3,A4,FINSEQ_2:10; end; theorem F[;](d,p'^q') = (F[;](d,p'))^(F[;](d,q')) proof defpred P[FinSequence of D'] means F[;](d,p'^($1)) = (F[;](d,p'))^(F[;](d,$1)); F[;](d,p'^(<*>D')) = F[;](d,p') by FINSEQ_1:47 .= (F[;](d,p'))^(<*>E) by FINSEQ_1:47 .= (F[;](d,p'))^(F[;](d,<*>D')) by FINSEQ_2:93; then A1: P[<*>D']; A2: for q',d' st P[q'] holds P[q'^<*d'*>] proof let q',d' such that A3: F[;](d,p'^q') = (F[;](d,p'))^(F[;](d,q')); thus F[;](d,p'^(q'^<*d'*>)) = F[;](d,(p'^q')^<*d'*>) by FINSEQ_1:45 .= (F[;](d,p'^q'))^<*F.(d,d')*> by Th13 .= (F[;](d,p'))^((F[;](d,q'))^<*F.(d,d')*>) by A3,FINSEQ_1:45 .= (F[;](d,p'))^(F[;](d,q'^<*d'*>)) by Th13; end; for q' holds P[q'] from IndSeqD(A1,A2); hence thesis; end; theorem Th15: F[:](p^<*d*>,d') = (F[:](p,d'))^<*F.(d,d')*> proof set pd = p^<*d*>, q = F[:](p,d'); set r = F[:](pd,d'), s = q^<*F.(d,d')*>; set i = len p; A1: len pd = i + 1 by FINSEQ_2:19; A2: len q = i by FINSEQ_2:98; A3: len r = i + 1 by A1,FINSEQ_2:98; A4: len s = len q + 1 by FINSEQ_2:19; now let j; assume A5: j in Seg(i+1); then A6: j in dom r by A3,FINSEQ_1:def 3; now per cases by A5,FINSEQ_2:8; suppose A7: j in Seg i; then A8: j in dom q by A2,FINSEQ_1:def 3; Seg len p = dom p by FINSEQ_1:def 3; hence F.(pd.j,d') = F.(p.j,d') by A7,FINSEQ_1:def 7 .= q.j by A8,FUNCOP_1:35 .= s.j by A8,FINSEQ_1:def 7; suppose A9: j = i+1; hence F.(pd.j,d') = F.(d,d') by FINSEQ_1:59 .= s.j by A2,A9,FINSEQ_1:59; end; hence r.j = s.j by A6,FUNCOP_1:35; end; hence thesis by A2,A3,A4,FINSEQ_2:10; end; theorem F[:](p^q,d') = (F[:](p,d'))^(F[:](q,d')) proof defpred P[FinSequence of D] means F[:](p^($1),d') = (F[:](p,d'))^(F[:]($1,d')); F[:](p^(<*>D),d') = F[:](p,d') by FINSEQ_1:47 .= (F[:](p,d'))^(<*>E) by FINSEQ_1:47 .= (F[:](p,d'))^(F[:](<*>D,d')) by FINSEQ_2:99; then A1: P[<*>D]; A2: for q,d st P[q] holds P[q^<*d*>] proof let q,d such that A3: F[:](p^q,d') = (F[:](p,d'))^(F[:](q,d')); thus F[:](p^(q^<*d*>),d') = F[:]((p^q)^<*d*>,d') by FINSEQ_1:45 .= (F[:](p^q,d'))^<*F.(d,d')*> by Th15 .= (F[:](p,d'))^((F[:](q,d'))^<*F.(d,d')*>) by A3,FINSEQ_1:45 .= (F[:](p,d'))^(F[:](q^<*d*>,d')) by Th15; end; for q holds P[q] from IndSeqD(A1,A2); hence thesis; end; theorem for h being Function of D,E holds h*(i|->d) = i|->(h.d) proof let h be Function of D,E; d in D; then d in dom h by FUNCT_2:def 1; then h*((Seg i)-->d) = (Seg i) --> (h.d) by FUNCOP_1:23; hence h*(i|->d) = (Seg i) --> (h.d) by FINSEQ_2:def 2 .= i|->(h.d) by FINSEQ_2:def 2; end; theorem Th18: F.:(i|->d,i|->d') = i |-> (F.(d,d')) proof [d,d'] in [:D,D':] by ZFMISC_1:def 2; then [d,d'] in dom F & i|->d = (Seg i)-->d & i|->d' = (Seg i)-->d' by FINSEQ_2:def 2,FUNCT_2:def 1; hence F.:(i|->d,i|->d') = (Seg i) --> (F.[d,d']) by Th8 .= (Seg i) --> (F.(d,d')) by BINOP_1:def 1 .= i |-> (F.(d,d')) by FINSEQ_2:def 2; end; theorem F[;](d,i|->d') = i |-> (F.(d,d')) proof thus F[;](d,i|->d') = F.:(dom(i|->d')-->d,i|->d') by FUNCOP_1:41 .= F.:(Seg i -->d,i|->d') by FINSEQ_2:68 .= F.:(i |->d,i|->d') by FINSEQ_2:def 2 .= i |-> (F.(d,d')) by Th18; end; theorem F[:](i|->d,d') = i |-> (F.(d,d')) proof thus F[:](i|->d,d') = F.:(i|->d,dom(i|->d)-->d') by FUNCOP_1:34 .= F.:(i|->d,Seg i-->d') by FINSEQ_2:68 .= F.:(i |->d,i|->d') by FINSEQ_2:def 2 .= i |-> (F.(d,d')) by Th18; end; theorem F.:(i|->d,T') = F[;](d,T') proof A1: dom T' = Seg len T' by FINSEQ_1:def 3 .= Seg i by FINSEQ_2:109; thus F.:(i|->d,T') = F.:((Seg i)-->d,T') by FINSEQ_2:def 2 .= F[;](d,T') by A1,FUNCOP_1:41; end; theorem F.:(T,i|->d) = F[:](T,d) proof A1: dom T = Seg len T by FINSEQ_1:def 3 .= Seg i by FINSEQ_2:109; thus F.:(T,i|->d) = F.:(T,(Seg i)-->d) by FINSEQ_2:def 2 .= F[:](T,d) by A1,FUNCOP_1:34; end; theorem F[;](d,T') = F[;](d,id D')*T' proof rng T' c= D' by FINSEQ_1:def 4; hence F[;](d,T') = F[;](d,(id D')*T') by RELAT_1:79 .= F[;](d,(id D'))*T' by FUNCOP_1:44; end; theorem F[:](T,d) = F[:](id D,d)*T proof rng T c= D by FINSEQ_1:def 4; hence F[:](T,d) = F[:]((id D)*T,d) by RELAT_1:79 .= F[:]((id D),d)*T by FUNCOP_1:37; end; :: Binary Operations reserve F,G for BinOp of D; reserve u for UnOp of D; reserve H for BinOp of E; Lm5: T is Function of Seg i,D proof len T = i by FINSEQ_2:109; then Seg i = dom T by FINSEQ_1:def 3; hence thesis by FINSEQ_2:30; end; theorem Th25: F is associative implies F[;](d,id D)*(F.:(f,f')) = F.:(F[;](d,id D)*f,f') proof assume A1: F is associative; now let c; thus (F[;](d,id D)*(F.:(f,f'))).c = (F[;](d,id D)).((F.:(f,f')).c) by FUNCT_2:21 .= (F[;](d,id D)).(F.(f.c,f'.c)) by FUNCOP_1:48 .= F.(d,(id D).(F.(f.c,f'.c))) by FUNCOP_1:66 .= F.(d,F.(f.c,f'.c)) by FUNCT_1:35 .= F.(F.(d,f.c),f'.c) by A1,BINOP_1:def 3 .= F.((F[;](d,f)).c,f'.c) by FUNCOP_1:66 .= F.(((F[;](d,id D))*f).c,f'.c) by FUNCOP_1:69 .= (F.:(F[;](d,id D)*f,f')).c by FUNCOP_1:48; end; hence thesis by FUNCT_2:113; end; theorem Th26: F is associative implies F[:](id D,d)*(F.:(f,f')) = F.:(f,F[:](id D,d)*f') proof assume A1: F is associative; now let c; thus (F[:](id D,d)*(F.:(f,f'))).c = (F[:](id D,d)).((F.:(f,f')).c) by FUNCT_2:21 .= (F[:](id D,d)).(F.(f.c,f'.c)) by FUNCOP_1:48 .= F.((id D).(F.(f.c,f'.c)),d) by FUNCOP_1:60 .= F.(F.(f.c,f'.c),d) by FUNCT_1:35 .= F.(f.c,F.(f'.c,d)) by A1,BINOP_1:def 3 .= F.(f.c,(F[:](f',d)).c) by FUNCOP_1:60 .= F.(f.c,((F[:](id D,d))*f').c) by FUNCOP_1:63 .= (F.:(f,F[:](id D,d)*f')).c by FUNCOP_1:48; end; hence thesis by FUNCT_2:113; end; theorem F is associative implies F[;](d,id D)*(F.:(T1,T2)) = F.:(F[;](d,id D)*T1,T2) proof assume A1: F is associative; per cases; suppose i = 0; then F.:(T1,T2) = <*>D & T2 = <*>D by Lm2,FINSEQ_2:113; then F[;](d,id D)*(F.:(T1,T2)) = <*>D & F.:(F[;](d,id D)*T1,T2) = <*>D by FINSEQ_2:38,87; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T1 is Function of C,D & T2 is Function of C,D by Lm5; hence thesis by A1,Th25; end; theorem F is associative implies F[:](id D,d)*(F.:(T1,T2)) = F.:(T1,F[:](id D,d)*T2) proof assume A1: F is associative; per cases; suppose i = 0; then F.:(T1,T2) = <*>D & T1 = <*>D by Lm2,FINSEQ_2:113; then F[:](id D,d)*(F.:(T1,T2)) = <*>D & F.:(T1,F[:](id D,d)*T2) = <*>D by FINSEQ_2:38,87; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T1 is Function of C,D & T2 is Function of C,D by Lm5; hence thesis by A1,Th26; end; theorem F is associative implies F.:(F.:(T1,T2),T3) = F.:(T1,F.:(T2,T3)) proof assume A1: F is associative; per cases; suppose i = 0; then F.:(T1,T2) = <*>D & F.:(T2,T3) = <*>D by Lm2; then F.:(F.:(T1,T2),T3) = <*>D & F.:(T1,F.: (T2,T3)) = <*>D by FINSEQ_2:87; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T1 is Function of C,D & T2 is Function of C,D & T3 is Function of C,D by Lm5; hence F.:(F.:(T1,T2),T3) = F.:(T1,F.:(T2,T3)) by A1,FUNCOP_1:76; end; theorem F is associative implies F[:](F[;](d1,T),d2) = F[;](d1,F[:](T,d2)) proof assume A1: F is associative; per cases; suppose i = 0; then F[;](d1,T) = <*>D & F[:](T,d2) = <*>D by Lm3,Lm4; then F[:](F[;](d1,T),d2) = <*>D & F[;](d1,F[:](T,d2)) = <*>D by FINSEQ_2:93,99; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D by Lm5; hence F[:](F[;](d1,T),d2) = F[;](d1,F[:](T,d2)) by A1,FUNCOP_1:74; end; theorem F is associative implies F.:(F[:](T1,d),T2) = F.:(T1,F[;](d,T2)) proof assume A1: F is associative; per cases; suppose i = 0; then F[:](T1,d) = <*>D & F[;](d,T2) = <*>D by Lm3,Lm4; then F.:(F[:](T1,d),T2) = <*>D & F.: (T1,F[;](d,T2)) = <*>D by FINSEQ_2:87; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T1 is Function of C,D & T2 is Function of C,D by Lm5; hence F.:(F[:](T1,d),T2) = F.:(T1,F[;](d,T2)) by A1,FUNCOP_1:75; end; theorem F is associative implies F[;](F.(d1,d2),T) = F[;](d1,F[;](d2,T)) proof assume A1: F is associative; per cases; suppose i = 0; then T = <*>D & F[;](d2,T) = <*>D by Lm3,FINSEQ_2:113; then F[;](F.(d1,d2),T) = <*>D & F[;](d1,F[;] (d2,T)) = <*>D by FINSEQ_2:93; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D by Lm5; hence F[;](F.(d1,d2),T) = F[;](d1,F[;](d2,T)) by A1,FUNCOP_1:77; end; theorem F is associative implies F[:](T,F.(d1,d2)) = F[:](F[:](T,d1),d2) proof assume A1: F is associative; per cases; suppose i = 0; then T = <*>D & F[:](T,d1) = <*>D by Lm4,FINSEQ_2:113; then F[:](T,F.(d1,d2)) = <*>D & F[:](F[:] (T,d1),d2) = <*>D by FINSEQ_2:99; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D by Lm5; hence F[:](T,F.(d1,d2)) = F[:](F[:](T,d1),d2) by A1,FUNCOP_1:78; end; theorem F is commutative implies F.:(T1,T2) = F.:(T2,T1) proof assume A1: F is commutative; per cases; suppose i = 0; then F.:(T1,T2) = <*>D & F.:(T2,T1) = <*>D by Lm2; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T1 is Function of C,D & T2 is Function of C,D by Lm5; hence F.:(T1,T2) = F.:(T2,T1) by A1,FUNCOP_1:80; end; theorem F is commutative implies F[;](d,T) = F[:](T,d) proof assume A1: F is commutative; per cases; suppose i = 0; then F[;](d,T) = <*>D & F[:](T,d) = <*>D by Lm3,Lm4; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D by Lm5; hence F[;](d,T) = F[:](T,d) by A1,FUNCOP_1:79; end; theorem Th36: F is_distributive_wrt G implies F[;](G.(d1,d2),f) = G.:(F[;](d1,f),F[;] (d2,f)) proof assume A1: F is_distributive_wrt G; now let c; thus (F[;](G.(d1,d2),f)).c = F.(G.(d1,d2),f.c) by FUNCOP_1:66 .= G.(F.(d1,f.c),F.(d2,f.c)) by A1,BINOP_1:23 .= G.(F[;](d1,f).c,F.(d2,f.c)) by FUNCOP_1:66 .= G.((F[;](d1,f)).c,(F[;](d2,f)).c) by FUNCOP_1:66 .= (G.:(F[;](d1,f),F[;](d2,f))).c by FUNCOP_1:48; end; hence thesis by FUNCT_2:113; end; theorem Th37: F is_distributive_wrt G implies F[:](f,G.(d1,d2)) = G.:(F[:](f,d1),F[:] (f,d2)) proof assume A1: F is_distributive_wrt G; now let c; thus (F[:](f,G.(d1,d2))).c = F.(f.c,G.(d1,d2)) by FUNCOP_1:60 .= G.(F.(f.c,d1),F.(f.c,d2)) by A1,BINOP_1:23 .= G.(F[:](f,d1).c,F.(f.c,d2)) by FUNCOP_1:60 .= G.((F[:](f,d1)).c,(F[:](f,d2)).c) by FUNCOP_1:60 .= (G.:(F[:](f,d1),F[:](f,d2))).c by FUNCOP_1:48; end; hence thesis by FUNCT_2:113; end; theorem Th38: (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F.:(f,f')) = H.:(h*f,h*f') proof assume A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2); now let c; thus (h*(F.:(f,f'))).c = h.((F.:(f,f')).c) by FUNCT_2:21 .= h.(F.(f.c,f'.c)) by FUNCOP_1:48 .= H.(h.(f.c),h.(f'.c)) by A1 .= H.((h*f).c,h.(f'.c)) by FUNCT_2:21 .= H.((h*f).c,(h*f').c) by FUNCT_2:21 .= (H.:(h*f,h*f')).c by FUNCOP_1:48; end; hence thesis by FUNCT_2:113; end; theorem Th39: (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F[;](d,f)) = H[;](h.d,h*f) proof assume A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2); A2: dom f = C by FUNCT_2:def 1; A3: dom h = D by FUNCT_2:def 1; A4: dom(h*f) = C by FUNCT_2:def 1; reconsider g = C --> d as Function of C,D by FUNCOP_1:58; thus h*(F[;](d,f)) = h*(F.:(g,f)) by A2,FUNCOP_1:41 .= H.:(h*g,h*f) by A1,Th38 .= H.:(C-->(h.d),h*f) by A3,FUNCOP_1:23 .= H[;](h.d,h*f) by A4,FUNCOP_1:41; end; theorem Th40: (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F[:](f,d)) = H[:](h*f,h.d) proof assume A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2); A2: dom f = C by FUNCT_2:def 1; A3: dom h = D by FUNCT_2:def 1; A4: dom(h*f) = C by FUNCT_2:def 1; reconsider g = C --> d as Function of C,D by FUNCOP_1:58; thus h*(F[:](f,d)) = h*(F.:(f,g)) by A2,FUNCOP_1:34 .= H.:(h*f,h*g) by A1,Th38 .= H.:(h*f,C-->h.d) by A3,FUNCOP_1:23 .= H[:](h*f,h.d) by A4,FUNCOP_1:34; end; theorem u is_distributive_wrt F implies u*(F.:(f,f')) = F.:(u*f,u*f') proof assume for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2); hence thesis by Th38; end; theorem u is_distributive_wrt F implies u*(F[;](d,f)) = F[;](u.d,u*f) proof assume for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2); hence thesis by Th39; end; theorem u is_distributive_wrt F implies u*(F[:](f,d)) = F[:](u*f,u.d) proof assume for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2); hence thesis by Th40; end; theorem Th44: F has_a_unity implies F.:(C-->the_unity_wrt F,f) = f & F.:(f,C-->the_unity_wrt F) = f proof assume A1: F has_a_unity; set e = the_unity_wrt F; reconsider g = C-->e as Function of C,D by FUNCOP_1:58; now let c; thus (F.:(g,f)).c = F.(g.c,f.c) by FUNCOP_1:48 .= F.(e,f.c) by FUNCOP_1:13 .= f.c by A1,SETWISEO:23; end; hence F.:(C-->e,f) = f by FUNCT_2:113; now let c; thus (F.:(f,g)).c = F.(f.c,g.c) by FUNCOP_1:48 .= F.(f.c,e) by FUNCOP_1:13 .= f.c by A1,SETWISEO:23; end; hence F.:(f,C-->e) = f by FUNCT_2:113; end; theorem Th45: F has_a_unity implies F[;](the_unity_wrt F,f) = f proof assume A1: F has_a_unity; set e = the_unity_wrt F; now let c; thus (F[;](e,f)).c = F.(e,f.c) by FUNCOP_1:66 .= f.c by A1,SETWISEO:23; end; hence thesis by FUNCT_2:113; end; theorem Th46: F has_a_unity implies F[:](f,the_unity_wrt F) = f proof assume A1: F has_a_unity; set e = the_unity_wrt F; now let c; thus (F[:](f,e)).c = F.(f.c,e) by FUNCOP_1:60 .= f.c by A1,SETWISEO:23; end; hence thesis by FUNCT_2:113; end; theorem F is_distributive_wrt G implies F[;](G.(d1,d2),T) = G.:(F[;](d1,T),F[;] (d2,T)) proof assume A1: F is_distributive_wrt G; per cases; suppose A2: i = 0; then F[;](d1,T) = <*>D by Lm3; then F[;](G.(d1,d2),T) = <*>D & G.:(F[;](d1,T),F[;](d2,T)) = <*>D by A2,Lm3,FINSEQ_2:87; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D by Lm5; hence thesis by A1,Th36; end; theorem F is_distributive_wrt G implies F[:](T,G.(d1,d2)) = G.:(F[:](T,d1),F[:] (T,d2)) proof assume A1: F is_distributive_wrt G; per cases; suppose A2: i = 0; then F[:](T,d1) = <*>D by Lm4; then F[:](T,G.(d1,d2)) = <*>D & G.:(F[:](T,d1),F[:](T,d2)) = <*>D by A2,Lm4,FINSEQ_2:87; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D by Lm5; hence thesis by A1,Th37; end; theorem Th49: (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F.:(T1,T2)) = H.:(h*T1,h*T2) proof assume A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2); per cases; suppose i = 0; then F.:(T1,T2) = <*>D & h*T1 = <*>E by Lm1,Lm2; then h*(F.:(T1,T2)) = <*>E & H.:(h*T1,h*T2) = <*>E by FINSEQ_2:38,87; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T1 is Function of C,D & T2 is Function of C,D by Lm5; hence thesis by A1,Th38; end; theorem Th50: (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F[;](d,T)) = H[;](h.d,h*T) proof assume A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2); per cases; suppose i = 0; then F[;](d,T) = <*>D & h*T = <*>E by Lm1,Lm3; then h*(F[;](d,T)) = <*>E & H[;] (h.d,h*T) = <*>E by FINSEQ_2:38,93; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D by Lm5; hence thesis by A1,Th39; end; theorem Th51: (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F[:](T,d)) = H[:](h*T,h.d) proof assume A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2); per cases; suppose i = 0; then F[:](T,d) = <*>D & h*T = <*>E by Lm1,Lm4; then h*(F[:](T,d)) = <*>E & H[:] (h*T,h.d) = <*>E by FINSEQ_2:38,99; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D by Lm5; hence thesis by A1,Th40; end; theorem u is_distributive_wrt F implies u*(F.:(T1,T2)) = F.:(u*T1,u*T2) proof assume for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2); hence thesis by Th49; end; theorem u is_distributive_wrt F implies u*(F[;](d,T)) = F[;](u.d,u*T) proof assume for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2); hence thesis by Th50; end; theorem u is_distributive_wrt F implies u*(F[:](T,d)) = F[:](u*T,u.d) proof assume for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2); hence thesis by Th51; end; theorem G is_distributive_wrt F & u = G[;](d,id D) implies u is_distributive_wrt F proof assume that A1: G is_distributive_wrt F and A2: u = G[;](d,id D); let d1,d2; thus u.(F.(d1,d2)) = G.(d,(id D).(F.(d1,d2))) by A2,FUNCOP_1:66 .= G.(d,F.(d1,d2)) by FUNCT_1:35 .= F.(G.(d,d1),G.(d,d2)) by A1,BINOP_1:23 .= F.(G.(d,(id D).d1),G.(d,d2)) by FUNCT_1:35 .= F.(G.(d,(id D).d1),G.(d,(id D).d2)) by FUNCT_1:35 .= F.(u.d1,G.(d,(id D).d2)) by A2,FUNCOP_1:66 .= F.(u.d1,u.d2) by A2,FUNCOP_1:66; end; theorem G is_distributive_wrt F & u = G[:](id D,d) implies u is_distributive_wrt F proof assume that A1: G is_distributive_wrt F and A2: u = G[:](id D,d); let d1,d2; thus u.(F.(d1,d2)) = G.((id D).(F.(d1,d2)),d) by A2,FUNCOP_1:60 .= G.(F.(d1,d2),d) by FUNCT_1:35 .= F.(G.(d1,d),G.(d2,d)) by A1,BINOP_1:23 .= F.(G.((id D).d1,d),G.(d2,d)) by FUNCT_1:35 .= F.(G.((id D).d1,d),G.((id D).d2,d)) by FUNCT_1:35 .= F.(u.d1,G.((id D).d2,d)) by A2,FUNCOP_1:60 .= F.(u.d1,u.d2) by A2,FUNCOP_1:60; end; theorem F has_a_unity implies F.:(i|->the_unity_wrt F,T) = T & F.:(T,i|->the_unity_wrt F) = T proof assume A1: F has_a_unity; set e = the_unity_wrt F; per cases; suppose i = 0; then F.:(i|->e,T) = <*>D & T = <*>D & F.:(T,i|->e) = <*>D by Lm2,FINSEQ_2:113; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D & i|->e = Seg i --> e by Lm5,FINSEQ_2:def 2; hence thesis by A1,Th44; end; theorem F has_a_unity implies F[;](the_unity_wrt F,T) = T proof assume A1: F has_a_unity; per cases; suppose i = 0; then T = <*>D & F[;](the_unity_wrt F,T) = <*>D by Lm3,FINSEQ_2:113; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D by Lm5; hence thesis by A1,Th45; end; theorem F has_a_unity implies F[:](T,the_unity_wrt F) = T proof assume A1: F has_a_unity; per cases; suppose i = 0; then T = <*>D & F[:](T,the_unity_wrt F) = <*>D by Lm4,FINSEQ_2:113; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D by Lm5; hence thesis by A1,Th46; end; definition let D,u,F; pred u is_an_inverseOp_wrt F means :Def1: for d holds F.(d,u.d) = the_unity_wrt F & F.(u.d,d) = the_unity_wrt F; end; definition let D,F; attr F is having_an_inverseOp means :Def2: ex u st u is_an_inverseOp_wrt F; synonym F has_an_inverseOp; end; definition let D,F; assume that A1: F has_a_unity and A2: F is associative and A3: F has_an_inverseOp; func the_inverseOp_wrt F -> UnOp of D means :Def3: it is_an_inverseOp_wrt F; existence by A3,Def2; uniqueness proof set e = the_unity_wrt F; let u1,u2 be UnOp of D such that A4: for d holds F.(d,u1.d) = e & F.(u1.d,d) = e and A5: for d holds F.(d,u2.d) = e & F.(u2.d,d) = e; now let d; set d1 = u1.d, d2 = u2.d; thus u1.d = F.(d1,e) by A1,SETWISEO:23 .= F.(d1,F.(d,d2)) by A5 .= F.(F.(d1,d),d2) by A2,BINOP_1:def 3 .= F.(e,d2) by A4 .= u2.d by A1,SETWISEO:23; end; hence thesis by FUNCT_2:113; end; end; canceled 3; theorem Th63: F has_a_unity & F is associative & F has_an_inverseOp implies F.((the_inverseOp_wrt F).d,d) = the_unity_wrt F & F.(d,(the_inverseOp_wrt F).d) = the_unity_wrt F proof assume F has_a_unity & F is associative & F has_an_inverseOp; then the_inverseOp_wrt F is_an_inverseOp_wrt F by Def3; hence thesis by Def1; end; theorem Th64: F has_a_unity & F is associative & F has_an_inverseOp & F.(d1,d2) = the_unity_wrt F implies d1 = (the_inverseOp_wrt F).d2 & (the_inverseOp_wrt F).d1 = d2 proof assume that A1: F has_a_unity & F is associative & F has_an_inverseOp and A2: F.(d1,d2) = the_unity_wrt F; set e = the_unity_wrt F, d3 = (the_inverseOp_wrt F).d2; F.(F.(d1,d2),d3) = d3 by A1,A2,SETWISEO:23; then F.(d1,F.(d2,d3)) = d3 by A1,BINOP_1:def 3; then F.(d1,e) = d3 by A1,Th63; hence d1 = d3 by A1,SETWISEO:23; set d3 = (the_inverseOp_wrt F).d1; F.(d3,F.(d1,d2)) = d3 by A1,A2,SETWISEO:23; then F.(F.(d3,d1),d2) = d3 by A1,BINOP_1:def 3; then F.(e,d2) = d3 by A1,Th63; hence d3 = d2 by A1,SETWISEO:23; end; theorem Th65: F has_a_unity & F is associative & F has_an_inverseOp implies (the_inverseOp_wrt F).(the_unity_wrt F) = the_unity_wrt F proof assume A1: F has_a_unity & F is associative & F has_an_inverseOp; set e = the_unity_wrt F; F.(e,e) = e by A1,SETWISEO:23; hence thesis by A1,Th64; end; theorem Th66: F has_a_unity & F is associative & F has_an_inverseOp implies (the_inverseOp_wrt F).((the_inverseOp_wrt F).d) = d proof assume A1: F has_a_unity & F is associative & F has_an_inverseOp; then F.(d,(the_inverseOp_wrt F).d) = the_unity_wrt F by Th63; hence thesis by A1,Th64; end; theorem Th67: F has_a_unity & F is associative & F is commutative & F has_an_inverseOp implies (the_inverseOp_wrt F) is_distributive_wrt F proof assume A1: F has_a_unity & F is associative & F is commutative & F has_an_inverseOp; set e = the_unity_wrt F, u = the_inverseOp_wrt F; let d1,d2; F.(F.(u.d1,u.d2),F.(d1,d2)) = F.(u.d1,F.(u.d2,F.(d1,d2))) by A1,BINOP_1:def 3 .= F.(u.d1,F.(F.(u.d2,d1),d2)) by A1,BINOP_1:def 3 .= F.(u.d1,F.(F.(d1,u.d2),d2)) by A1,BINOP_1:def 2 .= F.(u.d1,F.(d1,F.(u.d2,d2))) by A1,BINOP_1:def 3 .= F.(u.d1,F.(d1,e)) by A1,Th63 .= F.(F.(u.d1,d1),e) by A1,BINOP_1:def 3 .= F.(e,e) by A1,Th63 .= e by A1,SETWISEO:23; hence u.(F.(d1,d2)) = F.(u.d1,u.d2) by A1,Th64; end; theorem Th68: F has_a_unity & F is associative & F has_an_inverseOp & (F.(d,d1) = F.(d,d2) or F.(d1,d) = F.(d2,d)) implies d1 = d2 proof assume that A1: F has_a_unity & F is associative & F has_an_inverseOp and A2: F.(d,d1) = F.(d,d2) or F.(d1,d) = F.(d2,d); set e = the_unity_wrt F, u = the_inverseOp_wrt F; per cases by A2; suppose A3: F.(d,d1) = F.(d,d2); thus d1 = F.(e,d1) by A1,SETWISEO:23 .= F.(F.(u.d,d),d1) by A1,Th63 .= F.(u.d,F.(d,d2)) by A1,A3,BINOP_1:def 3 .= F.(F.(u.d,d),d2) by A1,BINOP_1:def 3 .= F.(e,d2) by A1,Th63 .= d2 by A1,SETWISEO:23; suppose A4: F.(d1,d) = F.(d2,d); thus d1 = F.(d1,e) by A1,SETWISEO:23 .= F.(d1,F.(d,u.d)) by A1,Th63 .= F.(F.(d2,d),u.d) by A1,A4,BINOP_1:def 3 .= F.(d2,F.(d,u.d)) by A1,BINOP_1:def 3 .= F.(d2,e) by A1,Th63 .= d2 by A1,SETWISEO:23; end; theorem Th69: F has_a_unity & F is associative & F has_an_inverseOp & (F.(d1,d2) = d2 or F.(d2,d1) = d2) implies d1 = the_unity_wrt F proof assume A1: F has_a_unity & F is associative & F has_an_inverseOp; set e = the_unity_wrt F; assume F.(d1,d2) = d2 or F.(d2,d1) = d2; then F.(d1,d2) = F.(e,d2) or F.(d2,d1) = F.(d2,e) by A1,SETWISEO:23; hence thesis by A1,Th68; end; theorem Th70: F is associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F & e = the_unity_wrt F implies for d holds G.(e,d) = e & G.(d,e) = e proof assume that A1: F is associative and A2: F has_a_unity and A3: F has_an_inverseOp and A4: G is_distributive_wrt F and A5: e = the_unity_wrt F; let d; set ed = G.(e,d); F.(ed,ed) = G.(F.(e,e),d) by A4,BINOP_1:23 .= ed by A2,A5,SETWISEO:23; hence ed = e by A1,A2,A3,A5,Th69; set de = G.(d,e); F.(de,de) = G.(d,F.(e,e)) by A4,BINOP_1:23 .= de by A2,A5,SETWISEO:23; hence de = e by A1,A2,A3,A5,Th69; end; theorem Th71: F has_a_unity & F is associative & F has_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F implies u.(G.(d1,d2)) = G.(u.d1,d2) & u.(G.(d1,d2)) = G.(d1,u.d2) proof assume that A1: F has_a_unity & F is associative & F has_an_inverseOp and A2: u = the_inverseOp_wrt F and A3: G is_distributive_wrt F; set e = the_unity_wrt F; F.(G.(d1,d2),G.(u.d1,d2)) = G.(F.(d1,u.d1),d2) by A3,BINOP_1:23 .= G.(e,d2) by A1,A2,Th63 .= e by A1,A3,Th70; hence u.(G.(d1,d2)) = G.(u.d1,d2) by A1,A2,Th64; F.(G.(d1,d2),G.(d1,u.d2)) = G.(d1,F.(d2,u.d2)) by A3,BINOP_1:23 .= G.(d1,e) by A1,A2,Th63 .= e by A1,A3,Th70; hence u.(G.(d1,d2)) = G.(d1,u.d2) by A1,A2,Th64; end; theorem F has_a_unity & F is associative & F has_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F & G has_a_unity implies G[;](u.(the_unity_wrt G),id D) = u proof assume that A1: F has_a_unity & F is associative & F has_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F and A2: G has_a_unity; set o = the_unity_wrt G; for d holds (G[;](u.o,id D)).d = u.d proof let d; thus (G[;](u.o,id D)).d = G.(u.o,(id D).d) by FUNCOP_1:66 .= G.(u.o,d) by FUNCT_1:35 .= u.(G.(o,d)) by A1,Th71 .= u.d by A2,SETWISEO:23; end; hence thesis by FUNCT_2:113; end; theorem F is associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F implies G[;](d,id D).the_unity_wrt F = the_unity_wrt F proof assume that A1: F is associative and A2: F has_a_unity and A3: F has_an_inverseOp and A4: G is_distributive_wrt F; set e = the_unity_wrt F, i = the_inverseOp_wrt F; G.(d,e) = G.(d,F.(e,e)) by A2,SETWISEO:23 .= F.(G.(d,e),G.(d,e)) by A4,BINOP_1:23; then e = F.(F.(G.(d,e),G.(d,e)),i.(G.(d,e))) by A1,A2,A3,Th63; then e = F.(G.(d,e),F.(G.(d,e),i.(G.(d,e)))) by A1,BINOP_1:def 3; then e = F.(G.(d,e),e) by A1,A2,A3,Th63; then e = G.(d,e) by A2,SETWISEO:23; then G.(d,(id D).e) = e by FUNCT_1:35; hence G[;](d,id D).e = e by FUNCOP_1:66; end; theorem F is associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F implies G[:](id D,d).the_unity_wrt F = the_unity_wrt F proof assume that A1: F is associative and A2: F has_a_unity and A3: F has_an_inverseOp and A4: G is_distributive_wrt F; set e = the_unity_wrt F, i = the_inverseOp_wrt F; G.(e,d) = G.(F.(e,e),d) by A2,SETWISEO:23 .= F.(G.(e,d),G.(e,d)) by A4,BINOP_1:23; then e = F.(F.(G.(e,d),G.(e,d)),i.(G.(e,d))) by A1,A2,A3,Th63; then e = F.(G.(e,d),F.(G.(e,d),i.(G.(e,d)))) by A1,BINOP_1:def 3; then e = F.(G.(e,d),e) by A1,A2,A3,Th63; then e = G.(e,d) by A2,SETWISEO:23; then G.((id D).e,d) = e by FUNCT_1:35; hence G[:](id D,d).e = e by FUNCOP_1:60; end; theorem Th75: F has_a_unity & F is associative & F has_an_inverseOp implies F.:(f,(the_inverseOp_wrt F)*f) = C-->the_unity_wrt F & F.:((the_inverseOp_wrt F)*f,f) = C-->the_unity_wrt F proof assume A1: F has_a_unity & F is associative & F has_an_inverseOp; set u = the_inverseOp_wrt F; reconsider g = C-->the_unity_wrt F as Function of C,D by FUNCOP_1:58; now let c; thus (F.:(f,u*f)).c = F.(f.c,(u*f).c) by FUNCOP_1:48 .= F.(f.c,u.(f.c)) by FUNCT_2:21 .= the_unity_wrt F by A1,Th63 .= g.c by FUNCOP_1:13; end; hence F.:(f,(the_inverseOp_wrt F)*f) = C-->the_unity_wrt F by FUNCT_2:113; now let c; thus (F.:(u*f,f)).c = F.((u*f).c,f.c) by FUNCOP_1:48 .= F.(u.(f.c),f.c) by FUNCT_2:21 .= the_unity_wrt F by A1,Th63 .= g.c by FUNCOP_1:13; end; hence thesis by FUNCT_2:113; end; theorem Th76: F is associative & F has_an_inverseOp & F has_a_unity & F.:(f,f') = C-->the_unity_wrt F implies f = (the_inverseOp_wrt F)*f' & (the_inverseOp_wrt F)*f = f' proof assume that A1: F is associative & F has_an_inverseOp & F has_a_unity and A2: F.:(f,f') = C-->the_unity_wrt F; set e = the_unity_wrt F; reconsider g = C-->e as Function of C,D by FUNCOP_1:58; set u = the_inverseOp_wrt F; now let c; F.(f.c,f'.c) = g.c by A2,FUNCOP_1:48 .= e by FUNCOP_1:13; hence f.c = u.(f'.c) by A1,Th64 .= (u*f').c by FUNCT_2:21; end; hence f = (the_inverseOp_wrt F)*f' by FUNCT_2:113; now let c; F.(f.c,f'.c) = g.c by A2,FUNCOP_1:48 .= e by FUNCOP_1:13; then f'.c = u.(f.c) by A1,Th64; hence (u*f).c = f'.c by FUNCT_2:21; end; hence thesis by FUNCT_2:113; end; theorem F has_a_unity & F is associative & F has_an_inverseOp implies F.:(T,(the_inverseOp_wrt F)*T) = i|->the_unity_wrt F & F.:((the_inverseOp_wrt F)*T,T) = i|->the_unity_wrt F proof assume A1: F has_a_unity & F is associative & F has_an_inverseOp; set e = the_unity_wrt F; reconsider uT = the_inverseOp_wrt F*T as Element of i-tuples_on D by FINSEQ_2:133; per cases; suppose i = 0; then F.:(T,uT) = <*>D & F.:(uT,T) = <*>D & i|->e = <*>D by Lm2,FINSEQ_2:113; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D & i|->e = C-->e by Lm5,FINSEQ_2:def 2; hence thesis by A1,Th75; end; theorem F is associative & F has_an_inverseOp & F has_a_unity & F.:(T1,T2) = i|->the_unity_wrt F implies T1 = (the_inverseOp_wrt F)*T2 & (the_inverseOp_wrt F)*T1 = T2 proof assume A1: F is associative & F has_an_inverseOp & F has_a_unity & F.:(T1,T2) = i|->the_unity_wrt F; per cases; suppose i = 0; then T1 = <*>D & (the_inverseOp_wrt F)*T2 = <*>D & (the_inverseOp_wrt F)*T1 = <*>D & T2 = <*>D by Lm1,FINSEQ_2:113; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T1 is Function of C,D & T2 is Function of C,D & i|->the_unity_wrt F = C-->the_unity_wrt F by Lm5,FINSEQ_2:def 2; hence thesis by A1,Th76; end; theorem Th79: F is associative & F has_a_unity & e = the_unity_wrt F & F has_an_inverseOp & G is_distributive_wrt F implies G[;](e,f) = C-->e proof assume A1: F is associative & F has_a_unity & e = the_unity_wrt F & F has_an_inverseOp & G is_distributive_wrt F; reconsider g = C-->e as Function of C,D by FUNCOP_1:58; now let c; thus (G[;](e,f)).c = G.(e,f.c) by FUNCOP_1:66 .= e by A1,Th70 .= g.c by FUNCOP_1:13; end; hence thesis by FUNCT_2:113; end; theorem F is associative & F has_a_unity & e = the_unity_wrt F & F has_an_inverseOp & G is_distributive_wrt F implies G[;](e,T) = i|->e proof assume A1: F is associative & F has_a_unity & e = the_unity_wrt F & F has_an_inverseOp & G is_distributive_wrt F; per cases; suppose i = 0; then G[;](e,T) = <*>D & i|->e = <*>D by Lm3,FINSEQ_2:113; hence thesis; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T is Function of C,D & i|->the_unity_wrt F = C-->the_unity_wrt F by Lm5,FINSEQ_2:def 2; hence thesis by A1,Th79; end; definition let F,f,g be Function; func F*(f,g) -> Function equals :Def4: F*[:f,g:]; correctness; end; canceled; theorem Th82: for F,f,g being Function st [x,y] in dom(F*(f,g)) holds (F*(f,g)).[x,y] = F.[f.x,g.y] proof let F,f,g be Function such that A1: [x,y] in dom(F*(f,g)); A2: F*(f,g) = F*[:f,g:] by Def4; then [x,y] in dom [:f,g:] by A1,FUNCT_1:21; then [x,y] in [:dom f,dom g:] by FUNCT_3:def 9; then [:f,g:].[x,y] = [f.x,g.y] by FUNCT_3:86; hence thesis by A1,A2,FUNCT_1:22; end; theorem Th83: for F,f,g being Function st [x,y] in dom(F*(f,g)) holds (F*(f,g)).(x,y) = F.(f.x,g.y) proof let F,f,g be Function; assume [x,y] in dom(F*(f,g)); then (F*(f,g)).[x,y] = F.[f.x,g.y] & F.[f.x,g.y] = F.(f.x,g.y) by Th82,BINOP_1:def 1; hence thesis by BINOP_1:def 1; end; theorem Th84: for F being Function of [:D,D':],E, f being Function of C,D, g being Function of C',D' holds F*(f,g) is Function of [:C,C':],E proof let F be Function of [:D,D':],E, f be Function of C,D, g be Function of C',D'; F*(f,g) = F*[:f,g:] by Def4; hence thesis; end; theorem for u,u' being Function of D,D holds F*(u,u') is BinOp of D by Th84; definition let D,F; let f,f' be Function of D,D; redefine func F*(f,f') -> BinOp of D; coherence by Th84; end; theorem Th86: for F being Function of [:D,D':],E, f being Function of C,D, g being Function of C',D' holds (F*(f,g)).(c,c') = F.(f.c,g.c') proof let F be Function of [:D,D':],E, f be Function of C,D, g be Function of C',D'; set H = F*(f,g); H is Function of [:C,C':],E by Th84; then dom H = [:C,C':] & c in C & c' in C' by FUNCT_2:def 1; then [c,c'] in dom H by ZFMISC_1:def 2; hence thesis by Th83; end; theorem Th87: for u being Function of D,D holds (F*(id D,u)).(d1,d2) = F.(d1,u.d2) & (F*(u,id D)).(d1,d2) = F.(u.d1,d2) proof let u be Function of D,D; (id D).d1 = d1 & (id D).d2 = d2 by FUNCT_1:35; hence thesis by Th86; end; theorem Th88: (F*(id D,u)).:(f,f') = F.:(f,u*f') proof now let c; thus ((F*(id D,u)).:(f,f')).c = (F*(id D,u)).(f.c,f'.c) by FUNCOP_1:48 .= F.(f.c,u.(f'.c)) by Th87 .= F.(f.c,(u*f').c) by FUNCT_2:21 .= (F.:(f,u*f')).c by FUNCOP_1:48; end; hence thesis by FUNCT_2:113; end; theorem (F*(id D,u)).:(T1,T2) = F.:(T1,u*T2) proof now per cases; suppose i = 0; then (F*(id D,u)).:(T1,T2) = <*>D & u*T2 = <*>D by Lm1,Lm2; hence thesis by FINSEQ_2:87; suppose i <> 0; then reconsider C = Seg i as non empty set by FINSEQ_1:5; T1 is Function of C,D & T2 is Function of C,D by Lm5; hence thesis by Th88; end; hence thesis; end; theorem F is associative & F has_a_unity & F is commutative & F has_an_inverseOp & u = the_inverseOp_wrt F implies u.(F*(id D,u).(d1,d2)) = F*(u,id D).(d1,d2) & F*(id D,u).(d1,d2) = u.(F*(u,id D).(d1,d2)) proof assume A1: F is associative & F has_a_unity & F is commutative & F has_an_inverseOp & u = the_inverseOp_wrt F; then A2: u is_distributive_wrt F by Th67; thus u.(F*(id D,u).(d1,d2)) = u.(F.(d1,u.d2)) by Th87 .= F.(u.d1,u.(u.d2)) by A2,BINOP_1:def 12 .= F.(u.d1,d2) by A1,Th66 .= F*(u,id D).(d1,d2) by Th87; hence F*(id D,u).(d1,d2) = u.(F*(u,id D).(d1,d2)) by A1,Th66; end; theorem F is associative & F has_a_unity & F has_an_inverseOp implies (F*(id D,the_inverseOp_wrt F)).(d,d) = the_unity_wrt F proof assume A1: F is associative & F has_a_unity & F has_an_inverseOp; set u = the_inverseOp_wrt F; thus F*(id D,u).(d,d) = F.(d,u.d) by Th87 .= the_unity_wrt F by A1,Th63; end; theorem F is associative & F has_a_unity & F has_an_inverseOp implies (F*(id D,the_inverseOp_wrt F)).(d,the_unity_wrt F) = d proof assume A1: F is associative & F has_a_unity & F has_an_inverseOp; set u = the_inverseOp_wrt F, e = the_unity_wrt F; thus (F*(id D,u)).(d,e) = F.(d,u.e) by Th87 .= F.(d,e) by A1,Th65 .= d by A1,SETWISEO:23; end; theorem F is associative & F has_a_unity & F has_an_inverseOp & u = the_inverseOp_wrt F implies (F*(id D,u)).(the_unity_wrt F,d) = u.d proof assume A1: F is associative & F has_a_unity & F has_an_inverseOp & u = the_inverseOp_wrt F; set e = the_unity_wrt F; thus (F*(id D,u)).(e,d) = F.(e,u.d) by Th87 .= u.d by A1,SETWISEO:23; end; theorem F is commutative & F is associative & F has_a_unity & F has_an_inverseOp & G = F*(id D,the_inverseOp_wrt F) implies for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4)) proof assume A1: F is commutative & F is associative & F has_a_unity & F has_an_inverseOp & G = F*(id D,the_inverseOp_wrt F); set u = the_inverseOp_wrt F; A2: u is_distributive_wrt F by A1,Th67; let d1,d2,d3,d4; thus F.(G.(d1,d2),G.(d3,d4)) = F.(F.(d1,u.d2),G.(d3,d4)) by A1,Th87 .= F.(F.(d1,u.d2),F.(d3,u.d4)) by A1,Th87 .= F.(d1,F.(u.d2,F.(d3,u.d4))) by A1,BINOP_1:def 3 .= F.(d1,F.(F.(u.d2,d3),u.d4)) by A1,BINOP_1:def 3 .= F.(d1,F.(F.(d3,u.d2),u.d4)) by A1,BINOP_1:def 2 .= F.(d1,F.(d3,F.(u.d2,u.d4))) by A1,BINOP_1:def 3 .= F.(F.(d1,d3),F.(u.d2,u.d4)) by A1,BINOP_1:def 3 .= F.(F.(d1,d3),u.(F.(d2,d4))) by A2,BINOP_1:def 12 .= G.(F.(d1,d3),F.(d2,d4)) by A1,Th87; end;

Back to top