:: Binary Operations Applied to Finite Sequences :: by Czes{\l}aw Byli\'nski :: :: Received May 4, 1990 :: Copyright (c) 1990-2019 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 XBOOLE_0, SUBSET_1, FUNCT_1, PARTFUN1, RELAT_1, ZFMISC_1, FUNCOP_1, TARSKI, NAT_1, FINSEQ_1, FINSEQ_2, ORDINAL4, ARYTM_3, CARD_1, BINOP_1, SETWISEO, FINSEQOP, ORDINAL1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, EQREL_1, FUNCT_1, FINSEQ_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3, FUNCOP_1, FINSEQ_2, SETWISEO; constructors PARTFUN1, BINOP_1, FUNCT_3, FUNCOP_1, SETWISEO, NAT_1, FINSEQ_2, RELSET_1, EQREL_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, NAT_1, FINSEQ_2, ORDINAL1, FINSEQ_1, CARD_1, RELSET_1; requirements NUMERALS, BOOLE, SUBSET; definitions BINOP_1; equalities BINOP_1, FUNCOP_1, FINSEQ_2; expansions BINOP_1; theorems ZFMISC_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSEQ_1, BINOP_1, SETWISEO, FINSEQ_2, FUNCT_3, RELAT_1, XBOOLE_0, CARD_1, TARSKI; schemes NAT_1, FINSEQ_2; begin reserve x,y for set; reserve C,C9,D,D9,E for non empty set; reserve c for Element of C; reserve c9 for Element of C9; reserve d,d1,d2,d3,d4,e for Element of D; reserve d9 for Element of D9; :: 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 7; hence thesis; 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 8; hence thesis by ZFMISC_1:90; end; theorem Th3: for F,f being Function holds F.:({},f) = {} & F.:(f,{}) = {} proof let F,f be Function; F.:({},f) = F*{} by Th1; hence thesis by Th1; end; theorem for F being Function holds F[:]({},x) = {} proof let F be Function; F[:]({},x) = F.:({}, dom {} --> x); hence thesis by Th3; end; theorem for F being Function holds F[;](x,{}) = {} proof let F be Function; F[;](x,{}) = F.:(dom {} --> x, {}); hence thesis by Th3; end; theorem Th6: 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 = {}; thus thesis by A1; end; suppose A2: X <> {}; rng fg c= [:{x1},{x2}:]; then A3: rng fg c= {[x1,x2]} by ZFMISC_1:29; set x = the Element of X; A4: dom f = X & dom g = X; then A5: dom fg = X by FUNCT_3:50; f.x = x1 & g.x = x2 by A2,FUNCOP_1:7; then fg.x = [x1,x2] by A2,A4,FUNCT_3:49; then [x1,x2] in rng fg by A2,A5,FUNCT_1:def 3; then {[x1,x2]} c= rng fg by ZFMISC_1:31; then rng fg = {[x1,x2]} by A3,XBOOLE_0:def 10; hence thesis by A5,FUNCOP_1:9; end; end; hence thesis; end; theorem Th7: 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*(X-->[x1,x2]) by Th6 .= X --> F.(x1,x2) by A1,FUNCOP_1:17; end; reserve i,j for natural Number; reserve F for Function of [:D,D9:],E; reserve p,q for FinSequence of D, p9,q9 for FinSequence of D9; definition let D,D9,E,F,p,p9; redefine func F.:(p,p9) -> FinSequence of E; coherence by FINSEQ_2:70; end; definition let D,D9,E,F,p,d9; redefine func F[:](p,d9) -> FinSequence of E; coherence by FINSEQ_2:83; end; definition let D,D9,E,F,d,p9; redefine func F[;](d,p9) -> FinSequence of E; coherence by FINSEQ_2:77; end; reserve f,f9 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:32; end; theorem Th8: 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:33; A2: len(h*p) = len p by FINSEQ_2:33; len(p^<*d*>) = i by FINSEQ_2:16; then A3: dom q = Seg i by A1,FINSEQ_1:def 3; A4: now let j be Nat; A5: Seg len p = dom p by FINSEQ_1:def 3; A6: Seg len(h*p) = dom(h*p) by FINSEQ_1:def 3; assume A7: j in dom q; now per cases by A3,A7,A5,FINSEQ_2:7; suppose A8: j in dom p; hence h.((p^<*d*>).j) = h.(p.j) by FINSEQ_1:def 7 .= (h*p).j by A2,A5,A6,A8,FUNCT_1:12 .= r.j by A2,A5,A6,A8,FINSEQ_1:def 7; end; suppose A9: j = i; hence h.((p^<*d*>).j) = h.d by FINSEQ_1:42 .= r.j by A2,A9,FINSEQ_1:42; end; end; hence q.j = r.j by A7,FUNCT_1:12; end; len r = len(h*p)+1 by FINSEQ_2:16; hence thesis by A1,A2,A4,FINSEQ_2:9,16; end; theorem h*(p^q) = (h*p)^(h*q) proof defpred P[FinSequence of D] means h*(p^\$1) = (h*p)^(h*\$1); A1: for q,d st P[q] holds P[q^<*d*>] proof let q,d such that A2: h*(p^q) = (h*p)^(h*q); thus h*(p^(q^<*d*>)) = h*((p^q)^<*d*>) by FINSEQ_1:32 .= (h*(p^q))^<*h.d*> by Th8 .= (h*p)^((h*q)^<*h.d*>) by A2,FINSEQ_1:32 .= (h*p)^(h*(q^<*d*>)) by Th8; end; h*(p^<*>D) = h*p by FINSEQ_1:34 .= (h*p)^(h*(<*>D)) by FINSEQ_1:34; then A3: P[<*>D]; for q holds P[q] from FINSEQ_2:sch 2(A3,A1); hence thesis; end; reserve T,T1,T2,T3 for Tuple of i,D; reserve T9 for Tuple of i, D9; reserve S for Tuple of j, D; reserve S9 for Tuple of j, D9; Lm1: for T being Tuple of 0, D holds F.:(T,T9) = <*>E proof let T be Tuple of 0, D; T = <*>D; hence thesis by FINSEQ_2:73; end; Lm2: for T9 being Tuple of 0, D9 holds F[;](d,T9) = <*>E proof let T9 be Tuple of 0, D9; T9 = <*>D9; hence thesis by FINSEQ_2:79; end; Lm3: for T being Tuple of 0, D holds F[:](T,d9) = <*>E proof let T be Tuple of 0, D; T = <*>D; hence thesis by FINSEQ_2:85; end; theorem Th10: F.:(T^<*d*>,T9^<*d9*>) = (F.:(T,T9))^<*F.(d,d9)*> proof set p = T^<*d*>, q = T9^<*d9*>, pq = F.:(T,T9); set r = F.:(p,q), s = pq^<*F.(d,d9)*>; A1: len T9 = i by CARD_1:def 7; then A2: len q = i+1 by FINSEQ_2:16; A3: len T = i by CARD_1:def 7; then A4: len pq = i by A1,FINSEQ_2:72; len p = i+1 by A3,FINSEQ_2:16; then A5: len r = i+1 by A2,FINSEQ_2:72; then A6: dom r = Seg(i+1) by FINSEQ_1:def 3; A7: now let j be Nat; assume A8: j in dom r; now per cases by A6,A8,FINSEQ_2:7; suppose A9: j in Seg i; Seg len T = dom T by FINSEQ_1:def 3; then A10: p.j = T.j by A3,A9,FINSEQ_1:def 7; A11: Seg len pq = dom pq by FINSEQ_1:def 3; Seg len T9 = dom T9 by FINSEQ_1:def 3; then A12: q.j = T9.j by A1,A9,FINSEQ_1:def 7; j in dom pq by A4,A9,FINSEQ_1:def 3; hence F.(p.j,q.j) = pq.j by A10,A12,FUNCOP_1:22 .= s.j by A4,A9,A11,FINSEQ_1:def 7; end; suppose A13: j = i+1; then p.j = d & q.j = d9 by A3,A1,FINSEQ_1:42; hence F.(p.j,q.j) = s.j by A4,A13,FINSEQ_1:42; end; end; hence r.j = s.j by A8,FUNCOP_1:22; end; len s = len pq + 1 by FINSEQ_2:16; hence thesis by A5,A4,A7,FINSEQ_2:9; end; theorem F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9)) proof A0: i is Nat & j is Nat by TARSKI:1; defpred P[Nat] means for S being Tuple of \$1, D, S9 being Tuple of \$1, D9 holds F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9)); now let j such that A1: for S,S9 holds F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9)); let S be Tuple of j+1, D; let S9 be Tuple of j+1, D9; consider S1 being Element of j-tuples_on D, d such that A2: S = S1^<*d*> by FINSEQ_2:117; A3: T^S = T^S1^<*d*> by A2,FINSEQ_1:32; reconsider S1 as Tuple of j, D; consider S19 being Element of j-tuples_on D9, d9 such that A4: S9 = S19^<*d9*> by FINSEQ_2:117; A5: T9^S9 = T9^S19^<*d9*> by A4,FINSEQ_1:32; reconsider S19 as Tuple of j, D9; thus F.:(T^S,T9^S9) = (F.:(T^S1,T9^S19))^<*F.(d,d9)*> by A3,A5,Th10 .= (F.:(T,T9))^(F.:(S1,S19))^<*F.(d,d9)*> by A1 .= (F.:(T,T9))^((F.:(S1,S19))^<*F.(d,d9)*>) by FINSEQ_1:32 .= (F.:(T,T9))^(F.:(S,S9)) by A2,A4,Th10; end; then A6: for j be Nat st P[j] holds P[j+1]; now let S be Tuple of 0, D; let S9 be Tuple of 0, D9; S = <*>D; then A7: F.:(S,S9) = <*>E by FINSEQ_2:73; T^S = T & T9^S9 = T9 by FINSEQ_2:95; hence F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9)) by A7,FINSEQ_1:34; end; then A8: P[0]; for j be Nat holds P[j] from NAT_1:sch 2(A8,A6); hence thesis by A0; end; theorem Th12: F[;](d,p9^<*d9*>) = (F[;](d,p9))^<*F.(d,d9)*> proof set pd = p9^<*d9*>, q = F[;](d,p9); set r = F[;](d,pd), s = q^<*F.(d,d9)*>; set i = len p9; A1: len q = i by FINSEQ_2:78; len pd = i + 1 by FINSEQ_2:16; then A2: len r = i + 1 by FINSEQ_2:78; then A3: dom r = Seg(i+1) by FINSEQ_1:def 3; A4: now let j be Nat; assume A5: j in dom r; now per cases by A3,A5,FINSEQ_2:7; suppose A6: j in Seg i; then A7: j in dom q by A1,FINSEQ_1:def 3; A8: Seg len q = dom q by FINSEQ_1:def 3; Seg len p9 = dom p9 by FINSEQ_1:def 3; hence F.(d,pd.j) = F.(d,p9.j) by A6,FINSEQ_1:def 7 .= q.j by A7,FUNCOP_1:32 .= s.j by A1,A6,A8,FINSEQ_1:def 7; end; suppose A9: j = i+1; hence F.(d,pd.j) = F.(d,d9) by FINSEQ_1:42 .= s.j by A1,A9,FINSEQ_1:42; end; end; hence r.j = s.j by A5,FUNCOP_1:32; end; len s = len q + 1 by FINSEQ_2:16; hence thesis by A1,A2,A4,FINSEQ_2:9; end; theorem F[;](d,p9^q9) = (F[;](d,p9))^(F[;](d,q9)) proof defpred P[FinSequence of D9] means F[;](d,p9^(\$1)) = (F[;](d,p9))^(F[;](d,\$1 )); A1: for q9,d9 st P[q9] holds P[q9^<*d9*>] proof let q9,d9 such that A2: F[;](d,p9^q9) = (F[;](d,p9))^(F[;](d,q9)); thus F[;](d,p9^(q9^<*d9*>)) = F[;](d,(p9^q9)^<*d9*>) by FINSEQ_1:32 .= (F[;](d,p9^q9))^<*F.(d,d9)*> by Th12 .= (F[;](d,p9))^((F[;](d,q9))^<*F.(d,d9)*>) by A2,FINSEQ_1:32 .= (F[;](d,p9))^(F[;](d,q9^<*d9*>)) by Th12; end; F[;](d,p9^(<*>D9)) = F[;](d,p9) by FINSEQ_1:34 .= (F[;](d,p9))^(<*>E) by FINSEQ_1:34 .= (F[;](d,p9))^(F[;](d,<*>D9)) by FINSEQ_2:79; then A3: P[<*>D9]; for q9 holds P[q9] from FINSEQ_2:sch 2(A3,A1); hence thesis; end; theorem Th14: F[:](p^<*d*>,d9) = (F[:](p,d9))^<*F.(d,d9)*> proof set pd = p^<*d*>, q = F[:](p,d9); set r = F[:](pd,d9), s = q^<*F.(d,d9)*>; set i = len p; A1: len q = i by FINSEQ_2:84; len pd = i + 1 by FINSEQ_2:16; then A2: len r = i + 1 by FINSEQ_2:84; then A3: dom r = Seg(i+1) by FINSEQ_1:def 3; A4: now let j be Nat; assume A5: j in dom r; now per cases by A3,A5,FINSEQ_2:7; suppose A6: j in Seg i; then A7: j in dom q by A1,FINSEQ_1:def 3; Seg len p = dom p by FINSEQ_1:def 3; hence F.(pd.j,d9) = F.(p.j,d9) by A6,FINSEQ_1:def 7 .= q.j by A7,FUNCOP_1:27 .= s.j by A7,FINSEQ_1:def 7; end; suppose A8: j = i+1; hence F.(pd.j,d9) = F.(d,d9) by FINSEQ_1:42 .= s.j by A1,A8,FINSEQ_1:42; end; end; hence r.j = s.j by A5,FUNCOP_1:27; end; len s = len q + 1 by FINSEQ_2:16; hence thesis by A1,A2,A4,FINSEQ_2:9; end; theorem F[:](p^q,d9) = (F[:](p,d9))^(F[:](q,d9)) proof defpred P[FinSequence of D] means F[:](p^(\$1),d9) = (F[:](p,d9))^(F[:](\$1,d9 )); A1: for q,d st P[q] holds P[q^<*d*>] proof let q,d such that A2: F[:](p^q,d9) = (F[:](p,d9))^(F[:](q,d9)); thus F[:](p^(q^<*d*>),d9) = F[:]((p^q)^<*d*>,d9) by FINSEQ_1:32 .= (F[:](p^q,d9))^<*F.(d,d9)*> by Th14 .= (F[:](p,d9))^((F[:](q,d9))^<*F.(d,d9)*>) by A2,FINSEQ_1:32 .= (F[:](p,d9))^(F[:](q^<*d*>,d9)) by Th14; end; F[:](p^(<*>D),d9) = F[:](p,d9) by FINSEQ_1:34 .= (F[:](p,d9))^(<*>E) by FINSEQ_1:34 .= (F[:](p,d9))^(F[:](<*>D,d9)) by FINSEQ_2:85; then A3: P[<*>D]; for q holds P[q] from FINSEQ_2:sch 2(A3,A1); 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; hence thesis by FUNCOP_1:17; end; theorem Th17: F.:(i|->d,i|->d9) = i |-> (F.(d,d9)) proof [d,d9] in [:D,D9:] by ZFMISC_1:def 2; then [d,d9] in dom F by FUNCT_2:def 1; hence thesis by Th7; end; theorem F[;](d,i|->d9) = i |-> (F.(d,d9)) proof thus F[;](d,i|->d9) = F.:(i |->d,i|->d9) .= i |-> (F.(d,d9)) by Th17; end; theorem F[:](i|->d,d9) = i |-> (F.(d,d9)) proof thus F[:](i|->d,d9) = F.:(i |->d,i|->d9) .= i |-> (F.(d,d9)) by Th17; end; theorem F.:(i|->d,T9) = F[;](d,T9) proof dom T9 = Seg len T9 by FINSEQ_1:def 3 .= Seg i by CARD_1:def 7; hence thesis; end; theorem F.:(T,i|->d) = F[:](T,d) proof dom T = Seg len T by FINSEQ_1:def 3 .= Seg i by CARD_1:def 7; hence thesis; end; theorem F[;](d,T9) = F[;](d,id D9)*T9 proof rng T9 c= D9; hence F[;](d,T9) = F[;](d,(id D9)*T9) by RELAT_1:53 .= F[;](d,(id D9))*T9 by FUNCOP_1:34; end; theorem F[:](T,d) = F[:](id D,d)*T proof rng T c= D; hence F[:](T,d) = F[:]((id D)*T,d) by RELAT_1:53 .= F[:]((id D),d)*T by FUNCOP_1:29; end; :: Binary Operations reserve F,G for BinOp of D; reserve u for UnOp of D; reserve H for BinOp of E; Lm4: T is Function of Seg i,D proof len T = i by CARD_1:def 7; then Seg i = dom T by FINSEQ_1:def 3; hence thesis by FINSEQ_2:26; end; theorem Th24: F is associative implies F[;](d,id D)*(F.:(f,f9)) = F.:(F[;](d, id D)*f,f9) proof assume A1: F is associative; now let c; thus (F[;](d,id D)*(F.:(f,f9))).c = (F[;](d,id D)).((F.:(f,f9)).c) by FUNCT_2:15 .= (F[;](d,id D)).(F.(f.c,f9.c)) by FUNCOP_1:37 .= F.(d,(id D).(F.(f.c,f9.c))) by FUNCOP_1:53 .= F.(d,F.(f.c,f9.c)) .= F.(F.(d,f.c),f9.c) by A1 .= F.((F[;](d,f)).c,f9.c) by FUNCOP_1:53 .= F.(((F[;](d,id D))*f).c,f9.c) by FUNCOP_1:55 .= (F.:(F[;](d,id D)*f,f9)).c by FUNCOP_1:37; end; hence thesis by FUNCT_2:63; end; theorem Th25: F is associative implies F[:](id D,d)*(F.:(f,f9)) = F.:(f,F[:]( id D,d)*f9) proof assume A1: F is associative; now let c; thus (F[:](id D,d)*(F.:(f,f9))).c = (F[:](id D,d)).((F.:(f,f9)).c) by FUNCT_2:15 .= (F[:](id D,d)).(F.(f.c,f9.c)) by FUNCOP_1:37 .= F.((id D).(F.(f.c,f9.c)),d) by FUNCOP_1:48 .= F.(F.(f.c,f9.c),d) .= F.(f.c,F.(f9.c,d)) by A1 .= F.(f.c,(F[:](f9,d)).c) by FUNCOP_1:48 .= F.(f.c,((F[:](id D,d))*f9).c) by FUNCOP_1:50 .= (F.:(f,F[:](id D,d)*f9)).c by FUNCOP_1:37; end; hence thesis by FUNCT_2:63; 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 A2: i = 0; then F.:(T1,T2) = <*>D by Lm1; then A3: F[;](d,id D)*(F.:(T1,T2)) = <*>D; T2 = <*>D by A2; hence thesis by A3,FINSEQ_2:73; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T1 is Function of C,D & T2 is Function of C,D by Lm4; hence thesis by A1,Th24; end; 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 A2: i = 0; then F.:(T1,T2) = <*>D by Lm1; then A3: F[:](id D,d)*(F.:(T1,T2)) = <*>D; T1 = <*>D by A2; hence thesis by A3,FINSEQ_2:73; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T1 is Function of C,D & T2 is Function of C,D by Lm4; hence thesis by A1,Th25; end; 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 A2: i = 0; then F.:(T1,T2) = <*>D by Lm1; then A3: F.:(F.:(T1,T2),T3) = <*>D by FINSEQ_2:73; F.:(T2,T3) = <*>D by A2,Lm1; hence thesis by A3,FINSEQ_2:73; end; suppose i <> 0; then reconsider C = Seg i as non empty set; A4: T3 is Function of C,D by Lm4; T1 is Function of C,D & T2 is Function of C,D by Lm4; hence thesis by A1,A4,FUNCOP_1:61; end; 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 A2: i = 0; then F[;](d1,T) = <*>D by Lm2; then A3: F[:](F[;](d1,T),d2) = <*>D by FINSEQ_2:85; F[:](T,d2) = <*>D by A2,Lm3; hence thesis by A3,FINSEQ_2:79; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,FUNCOP_1:59; end; 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 A2: i = 0; then F[:](T1,d) = <*>D by Lm3; then A3: F.:(F[:](T1,d),T2) = <*>D by FINSEQ_2:73; F[;](d,T2) = <*>D by A2,Lm2; hence thesis by A3,FINSEQ_2:73; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T1 is Function of C,D & T2 is Function of C,D by Lm4; hence thesis by A1,FUNCOP_1:60; end; 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 Lm2; hence thesis; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,FUNCOP_1:62; end; 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 Lm3; hence thesis; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,FUNCOP_1:63; end; end; theorem F is commutative implies F.:(T1,T2) = F.:(T2,T1) proof assume A1: F is commutative; per cases; suppose A2: i = 0; then F.:(T1,T2) = <*>D by Lm1; hence thesis by A2,Lm1; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T1 is Function of C,D & T2 is Function of C,D by Lm4; hence thesis by A1,FUNCOP_1:65; end; end; theorem F is commutative implies F[;](d,T) = F[:](T,d) proof assume A1: F is commutative; per cases; suppose A2: i = 0; then F[;](d,T) = <*>D by Lm2; hence thesis by A2,Lm3; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,FUNCOP_1:64; end; end; theorem Th35: 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:53 .= G.(F.(d1,f.c),F.(d2,f.c)) by A1,BINOP_1:11 .= G.(F[;](d1,f).c,F.(d2,f.c)) by FUNCOP_1:53 .= G.((F[;](d1,f)).c,(F[;](d2,f)).c) by FUNCOP_1:53 .= (G.:(F[;](d1,f),F[;](d2,f))).c by FUNCOP_1:37; end; hence thesis by FUNCT_2:63; end; theorem Th36: 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:48 .= G.(F.(f.c,d1),F.(f.c,d2)) by A1,BINOP_1:11 .= G.(F[:](f,d1).c,F.(f.c,d2)) by FUNCOP_1:48 .= G.((F[:](f,d1)).c,(F[:](f,d2)).c) by FUNCOP_1:48 .= (G.:(F[:](f,d1),F[:](f,d2))).c by FUNCOP_1:37; end; hence thesis by FUNCT_2:63; end; theorem Th37: (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F.:(f ,f9)) = H.:(h*f,h*f9) proof assume A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2); now let c; thus (h*(F.:(f,f9))).c = h.((F.:(f,f9)).c) by FUNCT_2:15 .= h.(F.(f.c,f9.c)) by FUNCOP_1:37 .= H.(h.(f.c),h.(f9.c)) by A1 .= H.((h*f).c,h.(f9.c)) by FUNCT_2:15 .= H.((h*f).c,(h*f9).c) by FUNCT_2:15 .= (H.:(h*f,h*f9)).c by FUNCOP_1:37; end; hence thesis by FUNCT_2:63; end; theorem Th38: (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); reconsider g = C --> d as Function of C,D; A2: dom h = D & dom(h*f) = C by FUNCT_2:def 1; thus h*(F[;](d,f)) = h*(F.:(g,f)) by FUNCT_2:def 1 .= H.:(h*g,h*f) by A1,Th37 .= H[;](h.d,h*f) by A2,FUNCOP_1:17; end; theorem Th39: (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); reconsider g = C --> d as Function of C,D; A2: dom h = D & dom(h*f) = C by FUNCT_2:def 1; thus h*(F[:](f,d)) = h*(F.:(f,g)) by FUNCT_2:def 1 .= H.:(h*f,h*g) by A1,Th37 .= H[:](h*f,h.d) by A2,FUNCOP_1:17; end; theorem u is_distributive_wrt F implies u*(F.:(f,f9)) = F.:(u*f,u*f9) by Th37; theorem u is_distributive_wrt F implies u*(F[;](d,f)) = F[;](u.d,u*f) by Th38; theorem u is_distributive_wrt F implies u*(F[:](f,d)) = F[:](u*f,u.d) by Th39; theorem Th43: F is having_a_unity implies F.:(C-->the_unity_wrt F,f) = f & F.: (f,C-->the_unity_wrt F) = f proof set e = the_unity_wrt F; reconsider g = C-->e as Function of C,D; assume A1: F is having_a_unity; now let c; thus (F.:(g,f)).c = F.(g.c,f.c) by FUNCOP_1:37 .= F.(e,f.c) .= f.c by A1,SETWISEO:15; end; hence F.:(C-->e,f) = f by FUNCT_2:63; now let c; thus (F.:(f,g)).c = F.(f.c,g.c) by FUNCOP_1:37 .= F.(f.c,e) .= f.c by A1,SETWISEO:15; end; hence thesis by FUNCT_2:63; end; theorem Th44: F is having_a_unity implies F[;](the_unity_wrt F,f) = f proof set e = the_unity_wrt F; assume A1: F is having_a_unity; now let c; thus (F[;](e,f)).c = F.(e,f.c) by FUNCOP_1:53 .= f.c by A1,SETWISEO:15; end; hence thesis by FUNCT_2:63; end; theorem Th45: F is having_a_unity implies F[:](f,the_unity_wrt F) = f proof set e = the_unity_wrt F; assume A1: F is having_a_unity; now let c; thus (F[:](f,e)).c = F.(f.c,e) by FUNCOP_1:48 .= f.c by A1,SETWISEO:15; end; hence thesis by FUNCT_2:63; 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 i = 0; then F[;](d1,T) = <*>D & F[;](G.(d1,d2),T) = <*>D by Lm2; hence thesis by FINSEQ_2:73; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,Th35; end; 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 i = 0; then F[:](T,d1) = <*>D & F[:](T,G.(d1,d2)) = <*>D by Lm3; hence thesis by FINSEQ_2:73; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,Th36; end; end; theorem Th48: (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 A2: i = 0; then F.:(T1,T2) = <*>D by Lm1; then A3: h*(F.:(T1,T2)) = <*>E; h*T1 = <*>E by A2; hence thesis by A3,FINSEQ_2:73; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T1 is Function of C,D & T2 is Function of C,D by Lm4; hence thesis by A1,Th37; end; end; theorem Th49: (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 A2: i = 0; then F[;](d,T) = <*>D by Lm2; then A3: h*(F[;](d,T)) = <*>E; h*T = <*>E by A2; hence thesis by A3,FINSEQ_2:79; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,Th38; end; end; theorem Th50: (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 A2: i = 0; then F[:](T,d) = <*>D by Lm3; then A3: h*(F[:](T,d)) = <*>E; h*T = <*>E by A2; hence thesis by A3,FINSEQ_2:85; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,Th39; end; end; theorem u is_distributive_wrt F implies u*(F.:(T1,T2)) = F.:(u*T1,u*T2) by Th48; theorem u is_distributive_wrt F implies u*(F[;](d,T)) = F[;](u.d,u*T) by Th49; theorem u is_distributive_wrt F implies u*(F[:](T,d)) = F[:](u*T,u.d) by Th50; 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:53 .= G.(d,F.(d1,d2)) .= F.(G.(d,d1),G.(d,d2)) by A1,BINOP_1:11 .= F.(G.(d,(id D).d1),G.(d,d2)) .= F.(G.(d,(id D).d1),G.(d,(id D).d2)) .= F.(u.d1,G.(d,(id D).d2)) by A2,FUNCOP_1:53 .= F.(u.d1,u.d2) by A2,FUNCOP_1:53; 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:48 .= G.(F.(d1,d2),d) .= F.(G.(d1,d),G.(d2,d)) by A1,BINOP_1:11 .= F.(G.((id D).d1,d),G.(d2,d)) .= F.(G.((id D).d1,d),G.((id D).d2,d)) .= F.(u.d1,G.((id D).d2,d)) by A2,FUNCOP_1:48 .= F.(u.d1,u.d2) by A2,FUNCOP_1:48; end; theorem F is having_a_unity implies F.:(i|->the_unity_wrt F,T) = T & F.:(T,i|->the_unity_wrt F) = T proof assume A1: F is having_a_unity; per cases; suppose A2: i = 0; then T = <*>D; hence thesis by A2,Lm1; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,Th43; end; end; theorem F is having_a_unity implies F[;](the_unity_wrt F,T) = T proof assume A1: F is having_a_unity; per cases; suppose i = 0; then T = <*>D; hence thesis by Lm2; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,Th44; end; end; theorem F is having_a_unity implies F[:](T,the_unity_wrt F) = T proof assume A1: F is having_a_unity; per cases; suppose i = 0; then T = <*>D; hence thesis by Lm3; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,Th45; end; end; definition let D,u,F; pred u is_an_inverseOp_wrt F means 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 ex u st u is_an_inverseOp_wrt F; end; definition let D,F; assume that A1: F is having_a_unity and A2: F is associative and A3: F is having_an_inverseOp; func the_inverseOp_wrt F -> UnOp of D means :Def3: it is_an_inverseOp_wrt F; existence by A3; 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:15 .= F.(d1,F.(d,d2)) by A5 .= F.(F.(d1,d),d2) by A2 .= F.(e,d2) by A4 .= u2.d by A1,SETWISEO:15; end; hence thesis by FUNCT_2:63; end; end; theorem Th59: F is having_a_unity & F is associative & F is having_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 is having_a_unity & F is associative & F is having_an_inverseOp; then the_inverseOp_wrt F is_an_inverseOp_wrt F by Def3; hence thesis; end; theorem Th60: F is having_a_unity & F is associative & F is having_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 is having_a_unity and A2: F is associative and A3: F is having_an_inverseOp and A4: 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,A4,SETWISEO:15; then F.(d1,F.(d2,d3)) = d3 by A2; then F.(d1,e) = d3 by A1,A2,A3,Th59; hence d1 = d3 by A1,SETWISEO:15; set d3 = (the_inverseOp_wrt F).d1; F.(d3,F.(d1,d2)) = d3 by A1,A4,SETWISEO:15; then F.(F.(d3,d1),d2) = d3 by A2; then F.(e,d2) = d3 by A1,A2,A3,Th59; hence thesis by A1,SETWISEO:15; end; theorem Th61: F is having_a_unity & F is associative & F is having_an_inverseOp implies (the_inverseOp_wrt F).(the_unity_wrt F) = the_unity_wrt F proof assume that A1: F is having_a_unity and A2: F is associative & F is having_an_inverseOp; set e = the_unity_wrt F; F.(e,e) = e by A1,SETWISEO:15; hence thesis by A1,A2,Th60; end; theorem Th62: F is having_a_unity & F is associative & F is having_an_inverseOp implies (the_inverseOp_wrt F).((the_inverseOp_wrt F).d) = d proof assume A1: F is having_a_unity & F is associative & F is having_an_inverseOp; then F.(d,(the_inverseOp_wrt F).d) = the_unity_wrt F by Th59; hence thesis by A1,Th60; end; theorem Th63: F is having_a_unity & F is associative & F is commutative & F is having_an_inverseOp implies (the_inverseOp_wrt F) is_distributive_wrt F proof assume that A1: F is having_a_unity and A2: F is associative and A3: F is commutative and A4: F is having_an_inverseOp; let d1,d2; set e = the_unity_wrt F, u = the_inverseOp_wrt F; F.(F.(u.d1,u.d2),F.(d1,d2)) = F.(u.d1,F.(u.d2,F.(d1,d2))) by A2 .= F.(u.d1,F.(F.(u.d2,d1),d2)) by A2 .= F.(u.d1,F.(F.(d1,u.d2),d2)) by A3 .= F.(u.d1,F.(d1,F.(u.d2,d2))) by A2 .= F.(u.d1,F.(d1,e)) by A1,A2,A4,Th59 .= F.(F.(u.d1,d1),e) by A2 .= F.(e,e) by A1,A2,A4,Th59 .= e by A1,SETWISEO:15; hence u.(F.(d1,d2)) = F.(u.d1,u.d2) by A1,A2,A4,Th60; end; theorem Th64: F is having_a_unity & F is associative & F is having_an_inverseOp & (F.(d,d1) = F.(d,d2) or F.(d1,d) = F.(d2,d)) implies d1 = d2 proof assume that A1: F is having_a_unity and A2: F is associative and A3: F is having_an_inverseOp and A4: 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 A4; suppose A5: F.(d,d1) = F.(d,d2); thus d1 = F.(e,d1) by A1,SETWISEO:15 .= F.(F.(u.d,d),d1) by A1,A2,A3,Th59 .= F.(u.d,F.(d,d2)) by A2,A5 .= F.(F.(u.d,d),d2) by A2 .= F.(e,d2) by A1,A2,A3,Th59 .= d2 by A1,SETWISEO:15; end; suppose A6: F.(d1,d) = F.(d2,d); thus d1 = F.(d1,e) by A1,SETWISEO:15 .= F.(d1,F.(d,u.d)) by A1,A2,A3,Th59 .= F.(F.(d2,d),u.d) by A2,A6 .= F.(d2,F.(d,u.d)) by A2 .= F.(d2,e) by A1,A2,A3,Th59 .= d2 by A1,SETWISEO:15; end; end; theorem Th65: F is having_a_unity & F is associative & F is having_an_inverseOp & (F.(d1,d2) = d2 or F.(d2,d1) = d2) implies d1 = the_unity_wrt F proof assume that A1: F is having_a_unity and A2: F is associative & F is having_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:15; hence thesis by A1,A2,Th64; end; theorem Th66: F is associative & F is having_a_unity & F is having_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 is having_a_unity and A3: F is having_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:11 .= ed by A2,A5,SETWISEO:15; hence ed = e by A1,A2,A3,A5,Th65; set de = G.(d,e); F.(de,de) = G.(d,F.(e,e)) by A4,BINOP_1:11 .= de by A2,A5,SETWISEO:15; hence thesis by A1,A2,A3,A5,Th65; end; theorem Th67: F is having_a_unity & F is associative & F is having_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 is having_a_unity & F is associative & F is having_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:11 .= G.(e,d2) by A1,A2,Th59 .= e by A1,A3,Th66; hence u.(G.(d1,d2)) = G.(u.d1,d2) by A1,A2,Th60; F.(G.(d1,d2),G.(d1,u.d2)) = G.(d1,F.(d2,u.d2)) by A3,BINOP_1:11 .= G.(d1,e) by A1,A2,Th59 .= e by A1,A3,Th66; hence thesis by A1,A2,Th60; end; theorem F is having_a_unity & F is associative & F is having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F & G is having_a_unity implies G [;](u.(the_unity_wrt G),id D) = u proof assume that A1: F is having_a_unity & F is associative & F is having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F and A2: G is having_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:53 .= G.(u.o,d) .= u.(G.(o,d)) by A1,Th67 .= u.d by A2,SETWISEO:15; end; hence thesis by FUNCT_2:63; end; theorem F is associative & F is having_a_unity & F is having_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 is having_a_unity and A3: F is having_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:15 .= F.(G.(d,e),G.(d,e)) by A4,BINOP_1:11; then e = F.(F.(G.(d,e),G.(d,e)),i.(G.(d,e))) by A1,A2,A3,Th59; then e = F.(G.(d,e),F.(G.(d,e),i.(G.(d,e)))) by A1; then e = F.(G.(d,e),e) by A1,A2,A3,Th59; then e = G.(d,e) by A2,SETWISEO:15; then G.(d,(id D).e) = e; hence thesis by FUNCOP_1:53; end; theorem F is associative & F is having_a_unity & F is having_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 is having_a_unity and A3: F is having_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:15 .= F.(G.(e,d),G.(e,d)) by A4,BINOP_1:11; then e = F.(F.(G.(e,d),G.(e,d)),i.(G.(e,d))) by A1,A2,A3,Th59; then e = F.(G.(e,d),F.(G.(e,d),i.(G.(e,d)))) by A1; then e = F.(G.(e,d),e) by A1,A2,A3,Th59; then e = G.(e,d) by A2,SETWISEO:15; then G.((id D).e,d) = e; hence thesis by FUNCOP_1:48; end; theorem Th71: F is having_a_unity & F is associative & F is having_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 set u = the_inverseOp_wrt F; reconsider g = C-->the_unity_wrt F as Function of C,D; assume A1: F is having_a_unity & F is associative & F is having_an_inverseOp; now let c; thus (F.:(f,u*f)).c = F.(f.c,(u*f).c) by FUNCOP_1:37 .= F.(f.c,u.(f.c)) by FUNCT_2:15 .= the_unity_wrt F by A1,Th59 .= g.c; end; hence F.:(f,(the_inverseOp_wrt F)*f) = C-->the_unity_wrt F by FUNCT_2:63; now let c; thus (F.:(u*f,f)).c = F.((u*f).c,f.c) by FUNCOP_1:37 .= F.(u.(f.c),f.c) by FUNCT_2:15 .= the_unity_wrt F by A1,Th59 .= g.c; end; hence thesis by FUNCT_2:63; end; theorem Th72: F is associative & F is having_an_inverseOp & F is having_a_unity & F.:(f,f9) = C-->the_unity_wrt F implies f = (the_inverseOp_wrt F)*f9 & (the_inverseOp_wrt F)*f = f9 proof assume that A1: F is associative & F is having_an_inverseOp & F is having_a_unity and A2: F.:(f,f9) = C-->the_unity_wrt F; set u = the_inverseOp_wrt F; set e = the_unity_wrt F; reconsider g = C-->e as Function of C,D; now let c; F.(f.c,f9.c) = g.c by A2,FUNCOP_1:37 .= e; hence f.c = u.(f9.c) by A1,Th60 .= (u*f9).c by FUNCT_2:15; end; hence f = (the_inverseOp_wrt F)*f9 by FUNCT_2:63; now let c; F.(f.c,f9.c) = g.c by A2,FUNCOP_1:37 .= e; then f9.c = u.(f.c) by A1,Th60; hence (u*f).c = f9.c by FUNCT_2:15; end; hence thesis by FUNCT_2:63; end; theorem F is having_a_unity & F is associative & F is having_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 is having_a_unity & F is associative & F is having_an_inverseOp; reconsider uT = the_inverseOp_wrt F*T as Element of i-tuples_on D by FINSEQ_2:113; per cases; suppose A2: i = 0; then F.:(T,uT) = <*>D & F.:(uT,T) = <*>D by Lm1; hence thesis by A2; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,Th71; end; end; theorem F is associative & F is having_an_inverseOp & F is having_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 is having_an_inverseOp & F is having_a_unity & F .:(T1,T2) = i|->the_unity_wrt F; per cases; suppose i = 0; then T1 = <*>D & T2 = <*>D; hence thesis; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T1 is Function of C,D & T2 is Function of C,D by Lm4; hence thesis by A1,Th72; end; end; theorem Th75: F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F implies G[;](e,f) = C-->e proof reconsider g = C-->e as Function of C,D; assume A1: F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F; now let c; thus (G[;](e,f)).c = G.(e,f.c) by FUNCOP_1:53 .= e by A1,Th66 .= g.c; end; hence thesis by FUNCT_2:63; end; theorem F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F implies G[;](e,T) = i|->e proof assume A1: F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F; per cases; suppose A2: i = 0; then G[;](e,T) = <*>D by Lm2; hence thesis by A2; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T is Function of C,D by Lm4; hence thesis by A1,Th75; end; end; definition let F,f,g be Function; func F*(f,g) -> Function equals F*[:f,g:]; correctness; end; theorem Th77: 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)); [x,y] in dom [:f,g:] by A1,FUNCT_1:11; then [x,y] in [:dom f,dom g:] by FUNCT_3:def 8; then [:f,g:].(x,y) = [f.x,g.y] by FUNCT_3:65; hence thesis by A1,FUNCT_1:12; end; ::\$CT theorem Th78: for F being Function of [:D,D9:],E, f being Function of C,D, g being Function of C9,D9 holds F*(f,g) is Function of [:C,C9:],E proof let F be Function of [:D,D9:],E, f be Function of C,D, g be Function of C9, D9; F*(f,g) = F*[:f,g:]; hence thesis; end; theorem for u,u9 being Function of D,D holds F*(u,u9) is BinOp of D by Th78; definition let D,F; let f,f9 be Function of D,D; redefine func F*(f,f9) -> BinOp of D; coherence by Th78; end; theorem Th80: for F being Function of [:D,D9:],E, f being Function of C,D, g being Function of C9,D9 holds (F*(f,g)).(c,c9) = F.(f.c,g.c9) proof let F be Function of [:D,D9:],E, f be Function of C,D, g be Function of C9, D9; set H = F*(f,g); H is Function of [:C,C9:],E by Th78; then dom H = [:C,C9:] by FUNCT_2:def 1; then [c,c9] in dom H by ZFMISC_1:def 2; hence thesis by Th77; end; theorem Th81: 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; hence thesis by Th80; end; theorem Th82: (F*(id D,u)).:(f,f9) = F.:(f,u*f9) proof now let c; thus ((F*(id D,u)).:(f,f9)).c = (F*(id D,u)).(f.c,f9.c) by FUNCOP_1:37 .= F.(f.c,u.(f9.c)) by Th81 .= F.(f.c,(u*f9).c) by FUNCT_2:15 .= (F.:(f,u*f9)).c by FUNCOP_1:37; end; hence thesis by FUNCT_2:63; 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; hence thesis by FINSEQ_2:73; end; suppose i <> 0; then reconsider C = Seg i as non empty set; T1 is Function of C,D & T2 is Function of C,D by Lm4; hence thesis by Th82; end; end; hence thesis; end; theorem F is associative & F is having_a_unity & F is commutative & F is having_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 that A1: F is associative & F is having_a_unity and A2: F is commutative and A3: F is having_an_inverseOp & u = the_inverseOp_wrt F; A4: u is_distributive_wrt F by A1,A2,A3,Th63; thus u.(F*(id D,u).(d1,d2)) = u.(F.(d1,u.d2)) by Th81 .= F.(u.d1,u.(u.d2)) by A4 .= F.(u.d1,d2) by A1,A3,Th62 .= F*(u,id D).(d1,d2) by Th81; hence thesis by A1,A3,Th62; end; theorem F is associative & F is having_a_unity & F is having_an_inverseOp implies (F*(id D,the_inverseOp_wrt F)).(d,d) = the_unity_wrt F proof assume A1: F is associative & F is having_a_unity & F is having_an_inverseOp; set u = the_inverseOp_wrt F; thus F*(id D,u).(d,d) = F.(d,u.d) by Th81 .= the_unity_wrt F by A1,Th59; end; theorem F is associative & F is having_a_unity & F is having_an_inverseOp implies (F*(id D,the_inverseOp_wrt F)).(d,the_unity_wrt F) = d proof assume that A1: F is associative and A2: F is having_a_unity and A3: F is having_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 Th81 .= F.(d,e) by A1,A2,A3,Th61 .= d by A2,SETWISEO:15; end; theorem F is having_a_unity implies (F*(id D,u)).(the_unity_wrt F,d) = u.d proof assume A1: F is having_a_unity; set e = the_unity_wrt F; thus (F*(id D,u)).(e,d) = F.(e,u.d) by Th81 .= u.d by A1,SETWISEO:15; end; theorem F is commutative & F is associative & F is having_a_unity & F is having_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 that A1: F is commutative and A2: F is associative and A3: F is having_a_unity & F is having_an_inverseOp and A4: G = F*(id D,the_inverseOp_wrt F); set u = the_inverseOp_wrt F; A5: u is_distributive_wrt F by A1,A2,A3,Th63; let d1,d2,d3,d4; thus F.(G.(d1,d2),G.(d3,d4)) = F.(F.(d1,u.d2),G.(d3,d4)) by A4,Th81 .= F.(F.(d1,u.d2),F.(d3,u.d4)) by A4,Th81 .= F.(d1,F.(u.d2,F.(d3,u.d4))) by A2 .= F.(d1,F.(F.(u.d2,d3),u.d4)) by A2 .= F.(d1,F.(F.(d3,u.d2),u.d4)) by A1 .= F.(d1,F.(d3,F.(u.d2,u.d4))) by A2 .= F.(F.(d1,d3),F.(u.d2,u.d4)) by A2 .= F.(F.(d1,d3),u.(F.(d2,d4))) by A5 .= G.(F.(d1,d3),F.(d2,d4)) by A4,Th81; end;