:: FINSEQOP semantic presentation begin theorem Th1: :: FINSEQOP:1 for f being Function holds ( <:{},f:> = {} & <:f,{}:> = {} ) proof let f be Function; ::_thesis: ( <:{},f:> = {} & <:f,{}:> = {} ) ( dom <:{},f:> = (dom {}) /\ (dom f) & dom <:f,{}:> = (dom f) /\ (dom {}) ) by FUNCT_3:def_7; hence ( <:{},f:> = {} & <:f,{}:> = {} ) ; ::_thesis: verum end; theorem :: FINSEQOP:2 for f being Function holds ( [:{},f:] = {} & [:f,{}:] = {} ) proof let f be Function; ::_thesis: ( [:{},f:] = {} & [:f,{}:] = {} ) ( dom [:{},f:] = [:(dom {}),(dom f):] & dom [:f,{}:] = [:(dom f),(dom {}):] ) by FUNCT_3:def_8; hence ( [:{},f:] = {} & [:f,{}:] = {} ) by ZFMISC_1:90; ::_thesis: verum end; theorem Th3: :: FINSEQOP:3 for F, f being Function holds ( F .: ({},f) = {} & F .: (f,{}) = {} ) proof let F, f be Function; ::_thesis: ( F .: ({},f) = {} & F .: (f,{}) = {} ) F .: ({},f) = F * {} by Th1; hence ( F .: ({},f) = {} & F .: (f,{}) = {} ) by Th1; ::_thesis: verum end; theorem :: FINSEQOP:4 for x being set for F being Function holds F [:] ({},x) = {} proof let x be set ; ::_thesis: for F being Function holds F [:] ({},x) = {} let F be Function; ::_thesis: F [:] ({},x) = {} F [:] ({},x) = F .: ({},((dom {}) --> x)) ; hence F [:] ({},x) = {} by Th3; ::_thesis: verum end; theorem :: FINSEQOP:5 for x being set for F being Function holds F [;] (x,{}) = {} proof let x be set ; ::_thesis: for F being Function holds F [;] (x,{}) = {} let F be Function; ::_thesis: F [;] (x,{}) = {} F [;] (x,{}) = F .: (((dom {}) --> x),{}) ; hence F [;] (x,{}) = {} by Th3; ::_thesis: verum end; theorem Th6: :: FINSEQOP:6 for X, x1, x2 being set holds <:(X --> x1),(X --> x2):> = X --> [x1,x2] proof let X be set ; ::_thesis: for x1, x2 being set holds <:(X --> x1),(X --> x2):> = X --> [x1,x2] let x1, x2 be set ; ::_thesis: <:(X --> x1),(X --> x2):> = X --> [x1,x2] set f = X --> x1; set g = X --> x2; set fg = <:(X --> x1),(X --> x2):>; now__::_thesis:_<:(X_-->_x1),(X_-->_x2):>_=_X_-->_[x1,x2] percases ( X = {} or X <> {} ) ; supposeA1: X = {} ; ::_thesis: <:(X --> x1),(X --> x2):> = X --> [x1,x2] thus <:(X --> x1),(X --> x2):> = X --> [x1,x2] by A1; ::_thesis: verum end; supposeA2: X <> {} ; ::_thesis: <:(X --> x1),(X --> x2):> = X --> [x1,x2] rng <:(X --> x1),(X --> x2):> c= [:{x1},{x2}:] ; then A3: rng <:(X --> x1),(X --> x2):> c= {[x1,x2]} by ZFMISC_1:29; set x = the Element of X; A4: ( dom (X --> x1) = X & dom (X --> x2) = X ) by FUNCOP_1:13; then A5: dom <:(X --> x1),(X --> x2):> = X by FUNCT_3:50; ( (X --> x1) . the Element of X = x1 & (X --> x2) . the Element of X = x2 ) by A2, FUNCOP_1:7; then <:(X --> x1),(X --> x2):> . the Element of X = [x1,x2] by A2, A4, FUNCT_3:49; then [x1,x2] in rng <:(X --> x1),(X --> x2):> by A2, A5, FUNCT_1:def_3; then {[x1,x2]} c= rng <:(X --> x1),(X --> x2):> by ZFMISC_1:31; then rng <:(X --> x1),(X --> x2):> = {[x1,x2]} by A3, XBOOLE_0:def_10; hence <:(X --> x1),(X --> x2):> = X --> [x1,x2] by A5, FUNCOP_1:9; ::_thesis: verum end; end; end; hence <:(X --> x1),(X --> x2):> = X --> [x1,x2] ; ::_thesis: verum end; theorem Th7: :: FINSEQOP:7 for F being Function for X, 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; ::_thesis: for X, x1, x2 being set st [x1,x2] in dom F holds F .: ((X --> x1),(X --> x2)) = X --> (F . (x1,x2)) let X be set ; ::_thesis: for x1, x2 being set st [x1,x2] in dom F holds F .: ((X --> x1),(X --> x2)) = X --> (F . (x1,x2)) let x1, x2 be set ; ::_thesis: ( [x1,x2] in dom F implies F .: ((X --> x1),(X --> x2)) = X --> (F . (x1,x2)) ) assume A1: [x1,x2] in dom F ; ::_thesis: F .: ((X --> x1),(X --> x2)) = X --> (F . (x1,x2)) set f = X --> x1; set g = X --> x2; thus F .: ((X --> x1),(X --> x2)) = F * (X --> [x1,x2]) by Th6 .= X --> (F . (x1,x2)) by A1, FUNCOP_1:17 ; ::_thesis: verum end; definition let D, D9, E be non empty set ; let F be Function of [:D,D9:],E; let p be FinSequence of D; let p9 be FinSequence of D9; :: original: .: redefine funcF .: (p,p9) -> FinSequence of E; coherence F .: (p,p9) is FinSequence of E by FINSEQ_2:70; end; definition let D, D9, E be non empty set ; let F be Function of [:D,D9:],E; let p be FinSequence of D; let d9 be Element of D9; :: original: [:] redefine funcF [:] (p,d9) -> FinSequence of E; coherence F [:] (p,d9) is FinSequence of E by FINSEQ_2:83; end; definition let D, D9, E be non empty set ; let F be Function of [:D,D9:],E; let d be Element of D; let p9 be FinSequence of D9; :: original: [;] redefine funcF [;] (d,p9) -> FinSequence of E; coherence F [;] (d,p9) is FinSequence of E by FINSEQ_2:77; end; definition let D, E be set ; let p be FinSequence of D; let h be Function of D,E; :: original: * redefine funch * p -> FinSequence of E; coherence p * h is FinSequence of E by FINSEQ_2:32; end; theorem Th8: :: FINSEQOP:8 for D, E being non empty set for d being Element of D for p being FinSequence of D for h being Function of D,E holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*> proof let D, E be non empty set ; ::_thesis: for d being Element of D for p being FinSequence of D for h being Function of D,E holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*> let d be Element of D; ::_thesis: for p being FinSequence of D for h being Function of D,E holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*> let p be FinSequence of D; ::_thesis: for h being Function of D,E holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*> let h be Function of D,E; ::_thesis: h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*> set q = h * (p ^ <*d*>); set r = (h * p) ^ <*(h . d)*>; set i = (len p) + 1; A1: len (h * (p ^ <*d*>)) = len (p ^ <*d*>) by FINSEQ_2:33; A2: len (h * p) = len p by FINSEQ_2:33; len (p ^ <*d*>) = (len p) + 1 by FINSEQ_2:16; then A3: dom (h * (p ^ <*d*>)) = Seg ((len p) + 1) by A1, FINSEQ_1:def_3; A4: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(h_*_(p_^_<*d*>))_holds_ (h_*_(p_^_<*d*>))_._j_=_((h_*_p)_^_<*(h_._d)*>)_._j let j be Nat; ::_thesis: ( j in dom (h * (p ^ <*d*>)) implies (h * (p ^ <*d*>)) . j = ((h * p) ^ <*(h . d)*>) . j ) 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 (h * (p ^ <*d*>)) ; ::_thesis: (h * (p ^ <*d*>)) . j = ((h * p) ^ <*(h . d)*>) . j now__::_thesis:_h_._((p_^_<*d*>)_._j)_=_((h_*_p)_^_<*(h_._d)*>)_._j percases ( j in dom p or j = (len p) + 1 ) by A3, A7, A5, FINSEQ_2:7; supposeA8: j in dom p ; ::_thesis: h . ((p ^ <*d*>) . j) = ((h * p) ^ <*(h . d)*>) . j hence h . ((p ^ <*d*>) . j) = h . (p . j) by FINSEQ_1:def_7 .= (h * p) . j by A2, A5, A6, A8, FUNCT_1:12 .= ((h * p) ^ <*(h . d)*>) . j by A2, A5, A6, A8, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA9: j = (len p) + 1 ; ::_thesis: h . ((p ^ <*d*>) . j) = ((h * p) ^ <*(h . d)*>) . j hence h . ((p ^ <*d*>) . j) = h . d by FINSEQ_1:42 .= ((h * p) ^ <*(h . d)*>) . j by A2, A9, FINSEQ_1:42 ; ::_thesis: verum end; end; end; hence (h * (p ^ <*d*>)) . j = ((h * p) ^ <*(h . d)*>) . j by A7, FUNCT_1:12; ::_thesis: verum end; len ((h * p) ^ <*(h . d)*>) = (len (h * p)) + 1 by FINSEQ_2:16; hence h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*> by A1, A2, A4, FINSEQ_2:9, FINSEQ_2:16; ::_thesis: verum end; theorem :: FINSEQOP:9 for D, E being non empty set for p, q being FinSequence of D for h being Function of D,E holds h * (p ^ q) = (h * p) ^ (h * q) proof let D, E be non empty set ; ::_thesis: for p, q being FinSequence of D for h being Function of D,E holds h * (p ^ q) = (h * p) ^ (h * q) let p, q be FinSequence of D; ::_thesis: for h being Function of D,E holds h * (p ^ q) = (h * p) ^ (h * q) let h be Function of D,E; ::_thesis: h * (p ^ q) = (h * p) ^ (h * q) defpred S1[ FinSequence of D] means h * (p ^ \$1) = (h * p) ^ (h * \$1); A1: for q being FinSequence of D for d being Element of D st S1[q] holds S1[q ^ <*d*>] proof let q be FinSequence of D; ::_thesis: for d being Element of D st S1[q] holds S1[q ^ <*d*>] let d be Element of D; ::_thesis: ( S1[q] implies S1[q ^ <*d*>] ) assume A2: h * (p ^ q) = (h * p) ^ (h * q) ; ::_thesis: S1[q ^ <*d*>] 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 ; ::_thesis: verum end; h * (p ^ (<*> D)) = h * p by FINSEQ_1:34 .= (h * p) ^ (h * (<*> D)) by FINSEQ_1:34 ; then A3: S1[ <*> D] ; for q being FinSequence of D holds S1[q] from FINSEQ_2:sch_2(A3, A1); hence h * (p ^ q) = (h * p) ^ (h * q) ; ::_thesis: verum end; Lm1: for D9, D, E being non empty set for i being Nat for F being Function of [:D,D9:],E for T9 being Tuple of i,D9 for T being Tuple of 0 ,D holds F .: (T,T9) = <*> E proof let D9, D, E be non empty set ; ::_thesis: for i being Nat for F being Function of [:D,D9:],E for T9 being Tuple of i,D9 for T being Tuple of 0 ,D holds F .: (T,T9) = <*> E let i be Nat; ::_thesis: for F being Function of [:D,D9:],E for T9 being Tuple of i,D9 for T being Tuple of 0 ,D holds F .: (T,T9) = <*> E let F be Function of [:D,D9:],E; ::_thesis: for T9 being Tuple of i,D9 for T being Tuple of 0 ,D holds F .: (T,T9) = <*> E let T9 be Tuple of i,D9; ::_thesis: for T being Tuple of 0 ,D holds F .: (T,T9) = <*> E let T be Tuple of 0 ,D; ::_thesis: F .: (T,T9) = <*> E T = <*> D ; hence F .: (T,T9) = <*> E by FINSEQ_2:73; ::_thesis: verum end; Lm2: for D, D9, E being non empty set for d being Element of D for F being Function of [:D,D9:],E for T9 being Tuple of 0 ,D9 holds F [;] (d,T9) = <*> E proof let D, D9, E be non empty set ; ::_thesis: for d being Element of D for F being Function of [:D,D9:],E for T9 being Tuple of 0 ,D9 holds F [;] (d,T9) = <*> E let d be Element of D; ::_thesis: for F being Function of [:D,D9:],E for T9 being Tuple of 0 ,D9 holds F [;] (d,T9) = <*> E let F be Function of [:D,D9:],E; ::_thesis: for T9 being Tuple of 0 ,D9 holds F [;] (d,T9) = <*> E let T9 be Tuple of 0 ,D9; ::_thesis: F [;] (d,T9) = <*> E T9 = <*> D9 ; hence F [;] (d,T9) = <*> E by FINSEQ_2:79; ::_thesis: verum end; Lm3: for D9, D, E being non empty set for d9 being Element of D9 for F being Function of [:D,D9:],E for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E proof let D9, D, E be non empty set ; ::_thesis: for d9 being Element of D9 for F being Function of [:D,D9:],E for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E let d9 be Element of D9; ::_thesis: for F being Function of [:D,D9:],E for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E let F be Function of [:D,D9:],E; ::_thesis: for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E let T be Tuple of 0 ,D; ::_thesis: F [:] (T,d9) = <*> E T = <*> D ; hence F [:] (T,d9) = <*> E by FINSEQ_2:85; ::_thesis: verum end; theorem Th10: :: FINSEQOP:10 for E, D, D9 being non empty set for d being Element of D for d9 being Element of D9 for i being Nat for F being Function of [:D,D9:],E for T being Tuple of i,D for T9 being Tuple of i,D9 holds F .: ((T ^ <*d*>),(T9 ^ <*d9*>)) = (F .: (T,T9)) ^ <*(F . (d,d9))*> proof let E, D, D9 be non empty set ; ::_thesis: for d being Element of D for d9 being Element of D9 for i being Nat for F being Function of [:D,D9:],E for T being Tuple of i,D for T9 being Tuple of i,D9 holds F .: ((T ^ <*d*>),(T9 ^ <*d9*>)) = (F .: (T,T9)) ^ <*(F . (d,d9))*> let d be Element of D; ::_thesis: for d9 being Element of D9 for i being Nat for F being Function of [:D,D9:],E for T being Tuple of i,D for T9 being Tuple of i,D9 holds F .: ((T ^ <*d*>),(T9 ^ <*d9*>)) = (F .: (T,T9)) ^ <*(F . (d,d9))*> let d9 be Element of D9; ::_thesis: for i being Nat for F being Function of [:D,D9:],E for T being Tuple of i,D for T9 being Tuple of i,D9 holds F .: ((T ^ <*d*>),(T9 ^ <*d9*>)) = (F .: (T,T9)) ^ <*(F . (d,d9))*> let i be Nat; ::_thesis: for F being Function of [:D,D9:],E for T being Tuple of i,D for T9 being Tuple of i,D9 holds F .: ((T ^ <*d*>),(T9 ^ <*d9*>)) = (F .: (T,T9)) ^ <*(F . (d,d9))*> let F be Function of [:D,D9:],E; ::_thesis: for T being Tuple of i,D for T9 being Tuple of i,D9 holds F .: ((T ^ <*d*>),(T9 ^ <*d9*>)) = (F .: (T,T9)) ^ <*(F . (d,d9))*> let T be Tuple of i,D; ::_thesis: for T9 being Tuple of i,D9 holds F .: ((T ^ <*d*>),(T9 ^ <*d9*>)) = (F .: (T,T9)) ^ <*(F . (d,d9))*> let T9 be Tuple of i,D9; ::_thesis: F .: ((T ^ <*d*>),(T9 ^ <*d9*>)) = (F .: (T,T9)) ^ <*(F . (d,d9))*> set p = T ^ <*d*>; set q = T9 ^ <*d9*>; set pq = F .: (T,T9); set r = F .: ((T ^ <*d*>),(T9 ^ <*d9*>)); set s = (F .: (T,T9)) ^ <*(F . (d,d9))*>; A1: len T9 = i by CARD_1:def_7; then A2: len (T9 ^ <*d9*>) = i + 1 by FINSEQ_2:16; A3: len T = i by CARD_1:def_7; then A4: len (F .: (T,T9)) = i by A1, FINSEQ_2:72; len (T ^ <*d*>) = i + 1 by A3, FINSEQ_2:16; then A5: len (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) = i + 1 by A2, FINSEQ_2:72; then A6: dom (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) = Seg (i + 1) by FINSEQ_1:def_3; A7: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(F_.:_((T_^_<*d*>),(T9_^_<*d9*>)))_holds_ (F_.:_((T_^_<*d*>),(T9_^_<*d9*>)))_._j_=_((F_.:_(T,T9))_^_<*(F_._(d,d9))*>)_._j let j be Nat; ::_thesis: ( j in dom (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) implies (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) . j = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j ) assume A8: j in dom (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) ; ::_thesis: (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) . j = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j now__::_thesis:_F_._(((T_^_<*d*>)_._j),((T9_^_<*d9*>)_._j))_=_((F_.:_(T,T9))_^_<*(F_._(d,d9))*>)_._j percases ( j in Seg i or j = i + 1 ) by A6, A8, FINSEQ_2:7; supposeA9: j in Seg i ; ::_thesis: F . (((T ^ <*d*>) . j),((T9 ^ <*d9*>) . j)) = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j Seg (len T) = dom T by FINSEQ_1:def_3; then A10: (T ^ <*d*>) . j = T . j by A3, A9, FINSEQ_1:def_7; A11: Seg (len (F .: (T,T9))) = dom (F .: (T,T9)) by FINSEQ_1:def_3; Seg (len T9) = dom T9 by FINSEQ_1:def_3; then A12: (T9 ^ <*d9*>) . j = T9 . j by A1, A9, FINSEQ_1:def_7; j in dom (F .: (T,T9)) by A4, A9, FINSEQ_1:def_3; hence F . (((T ^ <*d*>) . j),((T9 ^ <*d9*>) . j)) = (F .: (T,T9)) . j by A10, A12, FUNCOP_1:22 .= ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j by A4, A9, A11, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA13: j = i + 1 ; ::_thesis: F . (((T ^ <*d*>) . j),((T9 ^ <*d9*>) . j)) = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j then ( (T ^ <*d*>) . j = d & (T9 ^ <*d9*>) . j = d9 ) by A3, A1, FINSEQ_1:42; hence F . (((T ^ <*d*>) . j),((T9 ^ <*d9*>) . j)) = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j by A4, A13, FINSEQ_1:42; ::_thesis: verum end; end; end; hence (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) . j = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j by A8, FUNCOP_1:22; ::_thesis: verum end; len ((F .: (T,T9)) ^ <*(F . (d,d9))*>) = (len (F .: (T,T9))) + 1 by FINSEQ_2:16; hence F .: ((T ^ <*d*>),(T9 ^ <*d9*>)) = (F .: (T,T9)) ^ <*(F . (d,d9))*> by A5, A4, A7, FINSEQ_2:9; ::_thesis: verum end; theorem :: FINSEQOP:11 for E, D, D9 being non empty set for i, j being Nat for F being Function of [:D,D9:],E for T being Tuple of i,D for T9 being Tuple of i,D9 for S being Tuple of j,D for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) proof let E, D, D9 be non empty set ; ::_thesis: for i, j being Nat for F being Function of [:D,D9:],E for T being Tuple of i,D for T9 being Tuple of i,D9 for S being Tuple of j,D for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) let i, j be Nat; ::_thesis: for F being Function of [:D,D9:],E for T being Tuple of i,D for T9 being Tuple of i,D9 for S being Tuple of j,D for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) let F be Function of [:D,D9:],E; ::_thesis: for T being Tuple of i,D for T9 being Tuple of i,D9 for S being Tuple of j,D for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) let T be Tuple of i,D; ::_thesis: for T9 being Tuple of i,D9 for S being Tuple of j,D for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) let T9 be Tuple of i,D9; ::_thesis: for S being Tuple of j,D for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) let S be Tuple of j,D; ::_thesis: for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) let S9 be Tuple of j,D9; ::_thesis: F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) defpred S1[ Nat] means for S being Tuple of \$1,D for S9 being Tuple of \$1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)); now__::_thesis:_for_j_being_Nat_st_(_for_S_being_Tuple_of_j,D for_S9_being_Tuple_of_j,D9_holds_F_.:_((T_^_S),(T9_^_S9))_=_(F_.:_(T,T9))_^_(F_.:_(S,S9))_)_holds_ for_S_being_Tuple_of_j_+_1,D for_S9_being_Tuple_of_j_+_1,D9_holds_F_.:_((T_^_S),(T9_^_S9))_=_(F_.:_(T,T9))_^_(F_.:_(S,S9)) let j be Nat; ::_thesis: ( ( for S being Tuple of j,D for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) ) implies for S being Tuple of j + 1,D for S9 being Tuple of j + 1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) ) assume A1: for S being Tuple of j,D for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) ; ::_thesis: for S being Tuple of j + 1,D for S9 being Tuple of j + 1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) let S be Tuple of j + 1,D; ::_thesis: for S9 being Tuple of j + 1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) let S9 be Tuple of j + 1,D9; ::_thesis: F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) consider S1 being Element of j -tuples_on D, d being Element of D such that A2: S = S1 ^ <*d*> by FINSEQ_2:117; A3: T ^ S = (T ^ S1) ^ <*d*> by A2, FINSEQ_1:32; reconsider S1 = S1 as Tuple of j,D ; consider S19 being Element of j -tuples_on D9, d9 being Element of D9 such that A4: S9 = S19 ^ <*d9*> by FINSEQ_2:117; A5: T9 ^ S9 = (T9 ^ S19) ^ <*d9*> by A4, FINSEQ_1:32; reconsider S19 = S19 as Tuple of j,D9 ; ( T ^ S1 is Tuple of i + j,D & T9 ^ S19 is Tuple of i + j,D9 ) by FINSEQ_2:107; hence 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 ; ::_thesis: verum end; then A6: for j being Nat st S1[j] holds S1[j + 1] ; now__::_thesis:_for_S_being_Tuple_of_0_,D for_S9_being_Tuple_of_0_,D9_holds_F_.:_((T_^_S),(T9_^_S9))_=_(F_.:_(T,T9))_^_(F_.:_(S,S9)) let S be Tuple of 0 ,D; ::_thesis: for S9 being Tuple of 0 ,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) let S9 be Tuple of 0 ,D9; ::_thesis: F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) 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; ::_thesis: verum end; then A8: S1[ 0 ] ; for j being Nat holds S1[j] from NAT_1:sch_2(A8, A6); hence F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) ; ::_thesis: verum end; theorem Th12: :: FINSEQOP:12 for D, E, D9 being non empty set for d being Element of D for d9 being Element of D9 for F being Function of [:D,D9:],E for p9 being FinSequence of D9 holds F [;] (d,(p9 ^ <*d9*>)) = (F [;] (d,p9)) ^ <*(F . (d,d9))*> proof let D, E, D9 be non empty set ; ::_thesis: for d being Element of D for d9 being Element of D9 for F being Function of [:D,D9:],E for p9 being FinSequence of D9 holds F [;] (d,(p9 ^ <*d9*>)) = (F [;] (d,p9)) ^ <*(F . (d,d9))*> let d be Element of D; ::_thesis: for d9 being Element of D9 for F being Function of [:D,D9:],E for p9 being FinSequence of D9 holds F [;] (d,(p9 ^ <*d9*>)) = (F [;] (d,p9)) ^ <*(F . (d,d9))*> let d9 be Element of D9; ::_thesis: for F being Function of [:D,D9:],E for p9 being FinSequence of D9 holds F [;] (d,(p9 ^ <*d9*>)) = (F [;] (d,p9)) ^ <*(F . (d,d9))*> let F be Function of [:D,D9:],E; ::_thesis: for p9 being FinSequence of D9 holds F [;] (d,(p9 ^ <*d9*>)) = (F [;] (d,p9)) ^ <*(F . (d,d9))*> let p9 be FinSequence of D9; ::_thesis: F [;] (d,(p9 ^ <*d9*>)) = (F [;] (d,p9)) ^ <*(F . (d,d9))*> set pd = p9 ^ <*d9*>; set q = F [;] (d,p9); set r = F [;] (d,(p9 ^ <*d9*>)); set s = (F [;] (d,p9)) ^ <*(F . (d,d9))*>; set i = len p9; A1: len (F [;] (d,p9)) = len p9 by FINSEQ_2:78; len (p9 ^ <*d9*>) = (len p9) + 1 by FINSEQ_2:16; then A2: len (F [;] (d,(p9 ^ <*d9*>))) = (len p9) + 1 by FINSEQ_2:78; then A3: dom (F [;] (d,(p9 ^ <*d9*>))) = Seg ((len p9) + 1) by FINSEQ_1:def_3; A4: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(F_[;]_(d,(p9_^_<*d9*>)))_holds_ (F_[;]_(d,(p9_^_<*d9*>)))_._j_=_((F_[;]_(d,p9))_^_<*(F_._(d,d9))*>)_._j let j be Nat; ::_thesis: ( j in dom (F [;] (d,(p9 ^ <*d9*>))) implies (F [;] (d,(p9 ^ <*d9*>))) . j = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j ) assume A5: j in dom (F [;] (d,(p9 ^ <*d9*>))) ; ::_thesis: (F [;] (d,(p9 ^ <*d9*>))) . j = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j now__::_thesis:_F_._(d,((p9_^_<*d9*>)_._j))_=_((F_[;]_(d,p9))_^_<*(F_._(d,d9))*>)_._j percases ( j in Seg (len p9) or j = (len p9) + 1 ) by A3, A5, FINSEQ_2:7; supposeA6: j in Seg (len p9) ; ::_thesis: F . (d,((p9 ^ <*d9*>) . j)) = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j then A7: j in dom (F [;] (d,p9)) by A1, FINSEQ_1:def_3; A8: Seg (len (F [;] (d,p9))) = dom (F [;] (d,p9)) by FINSEQ_1:def_3; Seg (len p9) = dom p9 by FINSEQ_1:def_3; hence F . (d,((p9 ^ <*d9*>) . j)) = F . (d,(p9 . j)) by A6, FINSEQ_1:def_7 .= (F [;] (d,p9)) . j by A7, FUNCOP_1:32 .= ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j by A1, A6, A8, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA9: j = (len p9) + 1 ; ::_thesis: F . (d,((p9 ^ <*d9*>) . j)) = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j hence F . (d,((p9 ^ <*d9*>) . j)) = F . (d,d9) by FINSEQ_1:42 .= ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j by A1, A9, FINSEQ_1:42 ; ::_thesis: verum end; end; end; hence (F [;] (d,(p9 ^ <*d9*>))) . j = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j by A5, FUNCOP_1:32; ::_thesis: verum end; len ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) = (len (F [;] (d,p9))) + 1 by FINSEQ_2:16; hence F [;] (d,(p9 ^ <*d9*>)) = (F [;] (d,p9)) ^ <*(F . (d,d9))*> by A1, A2, A4, FINSEQ_2:9; ::_thesis: verum end; theorem :: FINSEQOP:13 for D, E, D9 being non empty set for d being Element of D for F being Function of [:D,D9:],E for p9, q9 being FinSequence of D9 holds F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9)) proof let D, E, D9 be non empty set ; ::_thesis: for d being Element of D for F being Function of [:D,D9:],E for p9, q9 being FinSequence of D9 holds F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9)) let d be Element of D; ::_thesis: for F being Function of [:D,D9:],E for p9, q9 being FinSequence of D9 holds F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9)) let F be Function of [:D,D9:],E; ::_thesis: for p9, q9 being FinSequence of D9 holds F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9)) let p9, q9 be FinSequence of D9; ::_thesis: F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9)) defpred S1[ FinSequence of D9] means F [;] (d,(p9 ^ \$1)) = (F [;] (d,p9)) ^ (F [;] (d,\$1)); A1: for q9 being FinSequence of D9 for d9 being Element of D9 st S1[q9] holds S1[q9 ^ <*d9*>] proof let q9 be FinSequence of D9; ::_thesis: for d9 being Element of D9 st S1[q9] holds S1[q9 ^ <*d9*>] let d9 be Element of D9; ::_thesis: ( S1[q9] implies S1[q9 ^ <*d9*>] ) assume A2: F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9)) ; ::_thesis: S1[q9 ^ <*d9*>] 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 ; ::_thesis: verum 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: S1[ <*> D9] ; for q9 being FinSequence of D9 holds S1[q9] from FINSEQ_2:sch_2(A3, A1); hence F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9)) ; ::_thesis: verum end; theorem Th14: :: FINSEQOP:14 for D9, E, D being non empty set for d being Element of D for d9 being Element of D9 for F being Function of [:D,D9:],E for p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*> proof let D9, E, D be non empty set ; ::_thesis: for d being Element of D for d9 being Element of D9 for F being Function of [:D,D9:],E for p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*> let d be Element of D; ::_thesis: for d9 being Element of D9 for F being Function of [:D,D9:],E for p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*> let d9 be Element of D9; ::_thesis: for F being Function of [:D,D9:],E for p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*> let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*> let p be FinSequence of D; ::_thesis: F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*> set pd = p ^ <*d*>; set q = F [:] (p,d9); set r = F [:] ((p ^ <*d*>),d9); set s = (F [:] (p,d9)) ^ <*(F . (d,d9))*>; set i = len p; A1: len (F [:] (p,d9)) = len p by FINSEQ_2:84; len (p ^ <*d*>) = (len p) + 1 by FINSEQ_2:16; then A2: len (F [:] ((p ^ <*d*>),d9)) = (len p) + 1 by FINSEQ_2:84; then A3: dom (F [:] ((p ^ <*d*>),d9)) = Seg ((len p) + 1) by FINSEQ_1:def_3; A4: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(F_[:]_((p_^_<*d*>),d9))_holds_ (F_[:]_((p_^_<*d*>),d9))_._j_=_((F_[:]_(p,d9))_^_<*(F_._(d,d9))*>)_._j let j be Nat; ::_thesis: ( j in dom (F [:] ((p ^ <*d*>),d9)) implies (F [:] ((p ^ <*d*>),d9)) . j = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j ) assume A5: j in dom (F [:] ((p ^ <*d*>),d9)) ; ::_thesis: (F [:] ((p ^ <*d*>),d9)) . j = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j now__::_thesis:_F_._(((p_^_<*d*>)_._j),d9)_=_((F_[:]_(p,d9))_^_<*(F_._(d,d9))*>)_._j percases ( j in Seg (len p) or j = (len p) + 1 ) by A3, A5, FINSEQ_2:7; supposeA6: j in Seg (len p) ; ::_thesis: F . (((p ^ <*d*>) . j),d9) = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j then A7: j in dom (F [:] (p,d9)) by A1, FINSEQ_1:def_3; Seg (len p) = dom p by FINSEQ_1:def_3; hence F . (((p ^ <*d*>) . j),d9) = F . ((p . j),d9) by A6, FINSEQ_1:def_7 .= (F [:] (p,d9)) . j by A7, FUNCOP_1:27 .= ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j by A7, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA8: j = (len p) + 1 ; ::_thesis: F . (((p ^ <*d*>) . j),d9) = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j hence F . (((p ^ <*d*>) . j),d9) = F . (d,d9) by FINSEQ_1:42 .= ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j by A1, A8, FINSEQ_1:42 ; ::_thesis: verum end; end; end; hence (F [:] ((p ^ <*d*>),d9)) . j = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j by A5, FUNCOP_1:27; ::_thesis: verum end; len ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) = (len (F [:] (p,d9))) + 1 by FINSEQ_2:16; hence F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*> by A1, A2, A4, FINSEQ_2:9; ::_thesis: verum end; theorem :: FINSEQOP:15 for D9, E, D being non empty set for d9 being Element of D9 for F being Function of [:D,D9:],E for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) proof let D9, E, D be non empty set ; ::_thesis: for d9 being Element of D9 for F being Function of [:D,D9:],E for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) let d9 be Element of D9; ::_thesis: for F being Function of [:D,D9:],E for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) let F be Function of [:D,D9:],E; ::_thesis: for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) let p, q be FinSequence of D; ::_thesis: F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) defpred S1[ FinSequence of D] means F [:] ((p ^ \$1),d9) = (F [:] (p,d9)) ^ (F [:] (\$1,d9)); A1: for q being FinSequence of D for d being Element of D st S1[q] holds S1[q ^ <*d*>] proof let q be FinSequence of D; ::_thesis: for d being Element of D st S1[q] holds S1[q ^ <*d*>] let d be Element of D; ::_thesis: ( S1[q] implies S1[q ^ <*d*>] ) assume A2: F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) ; ::_thesis: S1[q ^ <*d*>] 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 ; ::_thesis: verum 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: S1[ <*> D] ; for q being FinSequence of D holds S1[q] from FINSEQ_2:sch_2(A3, A1); hence F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) ; ::_thesis: verum end; theorem :: FINSEQOP:16 for D, E being non empty set for d being Element of D for i being Nat for h being Function of D,E holds h * (i |-> d) = i |-> (h . d) proof let D, E be non empty set ; ::_thesis: for d being Element of D for i being Nat for h being Function of D,E holds h * (i |-> d) = i |-> (h . d) let d be Element of D; ::_thesis: for i being Nat for h being Function of D,E holds h * (i |-> d) = i |-> (h . d) let i be Nat; ::_thesis: for h being Function of D,E holds h * (i |-> d) = i |-> (h . d) let h be Function of D,E; ::_thesis: h * (i |-> d) = i |-> (h . d) d in D ; then d in dom h by FUNCT_2:def_1; hence h * (i |-> d) = i |-> (h . d) by FUNCOP_1:17; ::_thesis: verum end; theorem Th17: :: FINSEQOP:17 for D, D9, E being non empty set for d being Element of D for d9 being Element of D9 for i being Nat for F being Function of [:D,D9:],E holds F .: ((i |-> d),(i |-> d9)) = i |-> (F . (d,d9)) proof let D, D9, E be non empty set ; ::_thesis: for d being Element of D for d9 being Element of D9 for i being Nat for F being Function of [:D,D9:],E holds F .: ((i |-> d),(i |-> d9)) = i |-> (F . (d,d9)) let d be Element of D; ::_thesis: for d9 being Element of D9 for i being Nat for F being Function of [:D,D9:],E holds F .: ((i |-> d),(i |-> d9)) = i |-> (F . (d,d9)) let d9 be Element of D9; ::_thesis: for i being Nat for F being Function of [:D,D9:],E holds F .: ((i |-> d),(i |-> d9)) = i |-> (F . (d,d9)) let i be Nat; ::_thesis: for F being Function of [:D,D9:],E holds F .: ((i |-> d),(i |-> d9)) = i |-> (F . (d,d9)) let F be Function of [:D,D9:],E; ::_thesis: F .: ((i |-> d),(i |-> d9)) = i |-> (F . (d,d9)) [d,d9] in [:D,D9:] by ZFMISC_1:def_2; then [d,d9] in dom F by FUNCT_2:def_1; hence F .: ((i |-> d),(i |-> d9)) = i |-> (F . (d,d9)) by Th7; ::_thesis: verum end; theorem :: FINSEQOP:18 for D, D9, E being non empty set for d being Element of D for d9 being Element of D9 for i being Nat for F being Function of [:D,D9:],E holds F [;] (d,(i |-> d9)) = i |-> (F . (d,d9)) proof let D, D9, E be non empty set ; ::_thesis: for d being Element of D for d9 being Element of D9 for i being Nat for F being Function of [:D,D9:],E holds F [;] (d,(i |-> d9)) = i |-> (F . (d,d9)) let d be Element of D; ::_thesis: for d9 being Element of D9 for i being Nat for F being Function of [:D,D9:],E holds F [;] (d,(i |-> d9)) = i |-> (F . (d,d9)) let d9 be Element of D9; ::_thesis: for i being Nat for F being Function of [:D,D9:],E holds F [;] (d,(i |-> d9)) = i |-> (F . (d,d9)) let i be Nat; ::_thesis: for F being Function of [:D,D9:],E holds F [;] (d,(i |-> d9)) = i |-> (F . (d,d9)) let F be Function of [:D,D9:],E; ::_thesis: F [;] (d,(i |-> d9)) = i |-> (F . (d,d9)) thus F [;] (d,(i |-> d9)) = F .: ((i |-> d),(i |-> d9)) by FUNCOP_1:13 .= i |-> (F . (d,d9)) by Th17 ; ::_thesis: verum end; theorem :: FINSEQOP:19 for D, D9, E being non empty set for d being Element of D for d9 being Element of D9 for i being Nat for F being Function of [:D,D9:],E holds F [:] ((i |-> d),d9) = i |-> (F . (d,d9)) proof let D, D9, E be non empty set ; ::_thesis: for d being Element of D for d9 being Element of D9 for i being Nat for F being Function of [:D,D9:],E holds F [:] ((i |-> d),d9) = i |-> (F . (d,d9)) let d be Element of D; ::_thesis: for d9 being Element of D9 for i being Nat for F being Function of [:D,D9:],E holds F [:] ((i |-> d),d9) = i |-> (F . (d,d9)) let d9 be Element of D9; ::_thesis: for i being Nat for F being Function of [:D,D9:],E holds F [:] ((i |-> d),d9) = i |-> (F . (d,d9)) let i be Nat; ::_thesis: for F being Function of [:D,D9:],E holds F [:] ((i |-> d),d9) = i |-> (F . (d,d9)) let F be Function of [:D,D9:],E; ::_thesis: F [:] ((i |-> d),d9) = i |-> (F . (d,d9)) thus F [:] ((i |-> d),d9) = F .: ((i |-> d),(i |-> d9)) by FUNCOP_1:13 .= i |-> (F . (d,d9)) by Th17 ; ::_thesis: verum end; theorem :: FINSEQOP:20 for D, E, D9 being non empty set for d being Element of D for i being Nat for F being Function of [:D,D9:],E for T9 being Tuple of i,D9 holds F .: ((i |-> d),T9) = F [;] (d,T9) proof let D, E, D9 be non empty set ; ::_thesis: for d being Element of D for i being Nat for F being Function of [:D,D9:],E for T9 being Tuple of i,D9 holds F .: ((i |-> d),T9) = F [;] (d,T9) let d be Element of D; ::_thesis: for i being Nat for F being Function of [:D,D9:],E for T9 being Tuple of i,D9 holds F .: ((i |-> d),T9) = F [;] (d,T9) let i be Nat; ::_thesis: for F being Function of [:D,D9:],E for T9 being Tuple of i,D9 holds F .: ((i |-> d),T9) = F [;] (d,T9) let F be Function of [:D,D9:],E; ::_thesis: for T9 being Tuple of i,D9 holds F .: ((i |-> d),T9) = F [;] (d,T9) let T9 be Tuple of i,D9; ::_thesis: F .: ((i |-> d),T9) = F [;] (d,T9) dom T9 = Seg (len T9) by FINSEQ_1:def_3 .= Seg i by CARD_1:def_7 ; hence F .: ((i |-> d),T9) = F [;] (d,T9) ; ::_thesis: verum end; theorem :: FINSEQOP:21 for D9, E, D being non empty set for d being Element of D for i being Nat for F being Function of [:D,D9:],E for T being Tuple of i,D holds F .: (T,(i |-> d)) = F [:] (T,d) proof let D9, E, D be non empty set ; ::_thesis: for d being Element of D for i being Nat for F being Function of [:D,D9:],E for T being Tuple of i,D holds F .: (T,(i |-> d)) = F [:] (T,d) let d be Element of D; ::_thesis: for i being Nat for F being Function of [:D,D9:],E for T being Tuple of i,D holds F .: (T,(i |-> d)) = F [:] (T,d) let i be Nat; ::_thesis: for F being Function of [:D,D9:],E for T being Tuple of i,D holds F .: (T,(i |-> d)) = F [:] (T,d) let F be Function of [:D,D9:],E; ::_thesis: for T being Tuple of i,D holds F .: (T,(i |-> d)) = F [:] (T,d) let T be Tuple of i,D; ::_thesis: F .: (T,(i |-> d)) = F [:] (T,d) dom T = Seg (len T) by FINSEQ_1:def_3 .= Seg i by CARD_1:def_7 ; hence F .: (T,(i |-> d)) = F [:] (T,d) ; ::_thesis: verum end; theorem :: FINSEQOP:22 for D, E, D9 being non empty set for d being Element of D for i being Nat for F being Function of [:D,D9:],E for T9 being Tuple of i,D9 holds F [;] (d,T9) = (F [;] (d,(id D9))) * T9 proof let D, E, D9 be non empty set ; ::_thesis: for d being Element of D for i being Nat for F being Function of [:D,D9:],E for T9 being Tuple of i,D9 holds F [;] (d,T9) = (F [;] (d,(id D9))) * T9 let d be Element of D; ::_thesis: for i being Nat for F being Function of [:D,D9:],E for T9 being Tuple of i,D9 holds F [;] (d,T9) = (F [;] (d,(id D9))) * T9 let i be Nat; ::_thesis: for F being Function of [:D,D9:],E for T9 being Tuple of i,D9 holds F [;] (d,T9) = (F [;] (d,(id D9))) * T9 let F be Function of [:D,D9:],E; ::_thesis: for T9 being Tuple of i,D9 holds F [;] (d,T9) = (F [;] (d,(id D9))) * T9 let T9 be Tuple of i,D9; ::_thesis: F [;] (d,T9) = (F [;] (d,(id D9))) * T9 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 ; ::_thesis: verum end; theorem :: FINSEQOP:23 for D9, E, D being non empty set for d being Element of D for i being Nat for F being Function of [:D,D9:],E for T being Tuple of i,D holds F [:] (T,d) = (F [:] ((id D),d)) * T proof let D9, E, D be non empty set ; ::_thesis: for d being Element of D for i being Nat for F being Function of [:D,D9:],E for T being Tuple of i,D holds F [:] (T,d) = (F [:] ((id D),d)) * T let d be Element of D; ::_thesis: for i being Nat for F being Function of [:D,D9:],E for T being Tuple of i,D holds F [:] (T,d) = (F [:] ((id D),d)) * T let i be Nat; ::_thesis: for F being Function of [:D,D9:],E for T being Tuple of i,D holds F [:] (T,d) = (F [:] ((id D),d)) * T let F be Function of [:D,D9:],E; ::_thesis: for T being Tuple of i,D holds F [:] (T,d) = (F [:] ((id D),d)) * T let T be Tuple of i,D; ::_thesis: F [:] (T,d) = (F [:] ((id D),d)) * T 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 ; ::_thesis: verum end; Lm4: for D being non empty set for i being Nat for T being Tuple of i,D holds T is Function of (Seg i),D proof let D be non empty set ; ::_thesis: for i being Nat for T being Tuple of i,D holds T is Function of (Seg i),D let i be Nat; ::_thesis: for T being Tuple of i,D holds T is Function of (Seg i),D let T be Tuple of i,D; ::_thesis: T is Function of (Seg i),D len T = i by CARD_1:def_7; then Seg i = dom T by FINSEQ_1:def_3; hence T is Function of (Seg i),D by FINSEQ_2:26; ::_thesis: verum end; theorem Th24: :: FINSEQOP:24 for C, D being non empty set for d being Element of D for f, f9 being Function of C,D for F being BinOp of D st F is associative holds (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9) proof let C, D be non empty set ; ::_thesis: for d being Element of D for f, f9 being Function of C,D for F being BinOp of D st F is associative holds (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9) let d be Element of D; ::_thesis: for f, f9 being Function of C,D for F being BinOp of D st F is associative holds (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9) let f, f9 be Function of C,D; ::_thesis: for F being BinOp of D st F is associative holds (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9) let F be BinOp of D; ::_thesis: ( F is associative implies (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9) ) assume A1: F is associative ; ::_thesis: (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9) now__::_thesis:_for_c_being_Element_of_C_holds_((F_[;]_(d,(id_D)))_*_(F_.:_(f,f9)))_._c_=_(F_.:_(((F_[;]_(d,(id_D)))_*_f),f9))_._c let c be Element of C; ::_thesis: ((F [;] (d,(id D))) * (F .: (f,f9))) . c = (F .: (((F [;] (d,(id D))) * f),f9)) . 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)))) by FUNCT_1:18 .= F . ((F . (d,(f . c))),(f9 . c)) by A1, BINOP_1:def_3 .= 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 ; ::_thesis: verum end; hence (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9) by FUNCT_2:63; ::_thesis: verum end; theorem Th25: :: FINSEQOP:25 for C, D being non empty set for d being Element of D for f, f9 being Function of C,D for F being BinOp of D st F is associative holds (F [:] ((id D),d)) * (F .: (f,f9)) = F .: (f,((F [:] ((id D),d)) * f9)) proof let C, D be non empty set ; ::_thesis: for d being Element of D for f, f9 being Function of C,D for F being BinOp of D st F is associative holds (F [:] ((id D),d)) * (F .: (f,f9)) = F .: (f,((F [:] ((id D),d)) * f9)) let d be Element of D; ::_thesis: for f, f9 being Function of C,D for F being BinOp of D st F is associative holds (F [:] ((id D),d)) * (F .: (f,f9)) = F .: (f,((F [:] ((id D),d)) * f9)) let f, f9 be Function of C,D; ::_thesis: for F being BinOp of D st F is associative holds (F [:] ((id D),d)) * (F .: (f,f9)) = F .: (f,((F [:] ((id D),d)) * f9)) let F be BinOp of D; ::_thesis: ( F is associative implies (F [:] ((id D),d)) * (F .: (f,f9)) = F .: (f,((F [:] ((id D),d)) * f9)) ) assume A1: F is associative ; ::_thesis: (F [:] ((id D),d)) * (F .: (f,f9)) = F .: (f,((F [:] ((id D),d)) * f9)) now__::_thesis:_for_c_being_Element_of_C_holds_((F_[:]_((id_D),d))_*_(F_.:_(f,f9)))_._c_=_(F_.:_(f,((F_[:]_((id_D),d))_*_f9)))_._c let c be Element of C; ::_thesis: ((F [:] ((id D),d)) * (F .: (f,f9))) . c = (F .: (f,((F [:] ((id D),d)) * f9))) . 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) by FUNCT_1:18 .= F . ((f . c),(F . ((f9 . c),d))) by A1, BINOP_1:def_3 .= 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 ; ::_thesis: verum end; hence (F [:] ((id D),d)) * (F .: (f,f9)) = F .: (f,((F [:] ((id D),d)) * f9)) by FUNCT_2:63; ::_thesis: verum end; theorem :: FINSEQOP:26 for D being non empty set for d being Element of D for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative holds (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) proof let D be non empty set ; ::_thesis: for d being Element of D for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative holds (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) let d be Element of D; ::_thesis: for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative holds (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) let i be Nat; ::_thesis: for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative holds (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) let T1, T2 be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative holds (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) let F be BinOp of D; ::_thesis: ( F is associative implies (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) ) assume A1: F is associative ; ::_thesis: (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) then F .: (T1,T2) = <*> D by Lm1; then A3: (F [;] (d,(id D))) * (F .: (T1,T2)) = <*> D ; T2 = <*> D by A2; hence (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) by A3, FINSEQ_2:73; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) then reconsider C = Seg i as non empty set ; ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4; hence (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) by A1, Th24; ::_thesis: verum end; end; end; theorem :: FINSEQOP:27 for D being non empty set for d being Element of D for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative holds (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) proof let D be non empty set ; ::_thesis: for d being Element of D for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative holds (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) let d be Element of D; ::_thesis: for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative holds (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) let i be Nat; ::_thesis: for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative holds (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) let T1, T2 be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative holds (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) let F be BinOp of D; ::_thesis: ( F is associative implies (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) ) assume A1: F is associative ; ::_thesis: (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) then F .: (T1,T2) = <*> D by Lm1; then A3: (F [:] ((id D),d)) * (F .: (T1,T2)) = <*> D ; T1 = <*> D by A2; hence (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) by A3, FINSEQ_2:73; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) then reconsider C = Seg i as non empty set ; ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4; hence (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) by A1, Th25; ::_thesis: verum end; end; end; theorem :: FINSEQOP:28 for D being non empty set for i being Nat for T1, T2, T3 being Tuple of i,D for F being BinOp of D st F is associative holds F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) proof let D be non empty set ; ::_thesis: for i being Nat for T1, T2, T3 being Tuple of i,D for F being BinOp of D st F is associative holds F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) let i be Nat; ::_thesis: for T1, T2, T3 being Tuple of i,D for F being BinOp of D st F is associative holds F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) let T1, T2, T3 be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative holds F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) let F be BinOp of D; ::_thesis: ( F is associative implies F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) ) assume A1: F is associative ; ::_thesis: F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) 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 F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) by A3, FINSEQ_2:73; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) 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 F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) by A1, A4, FUNCOP_1:61; ::_thesis: verum end; end; end; theorem :: FINSEQOP:29 for D being non empty set for d1, d2 being Element of D for i being Nat for T being Tuple of i,D for F being BinOp of D st F is associative holds F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) proof let D be non empty set ; ::_thesis: for d1, d2 being Element of D for i being Nat for T being Tuple of i,D for F being BinOp of D st F is associative holds F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) let d1, d2 be Element of D; ::_thesis: for i being Nat for T being Tuple of i,D for F being BinOp of D st F is associative holds F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) let i be Nat; ::_thesis: for T being Tuple of i,D for F being BinOp of D st F is associative holds F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative holds F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) let F be BinOp of D; ::_thesis: ( F is associative implies F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) ) assume A1: F is associative ; ::_thesis: F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) 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 F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) by A3, FINSEQ_2:79; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) by A1, FUNCOP_1:59; ::_thesis: verum end; end; end; theorem :: FINSEQOP:30 for D being non empty set for d being Element of D for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative holds F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) proof let D be non empty set ; ::_thesis: for d being Element of D for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative holds F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) let d be Element of D; ::_thesis: for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative holds F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) let i be Nat; ::_thesis: for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative holds F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) let T1, T2 be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative holds F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) let F be BinOp of D; ::_thesis: ( F is associative implies F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) ) assume A1: F is associative ; ::_thesis: F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) 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 F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) by A3, FINSEQ_2:73; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) then reconsider C = Seg i as non empty set ; ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4; hence F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) by A1, FUNCOP_1:60; ::_thesis: verum end; end; end; theorem :: FINSEQOP:31 for D being non empty set for d1, d2 being Element of D for i being Nat for T being Tuple of i,D for F being BinOp of D st F is associative holds F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) proof let D be non empty set ; ::_thesis: for d1, d2 being Element of D for i being Nat for T being Tuple of i,D for F being BinOp of D st F is associative holds F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) let d1, d2 be Element of D; ::_thesis: for i being Nat for T being Tuple of i,D for F being BinOp of D st F is associative holds F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) let i be Nat; ::_thesis: for T being Tuple of i,D for F being BinOp of D st F is associative holds F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative holds F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) let F be BinOp of D; ::_thesis: ( F is associative implies F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) ) assume A1: F is associative ; ::_thesis: F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) then ( T = <*> D & F [;] (d2,T) = <*> D ) by Lm2; hence F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) ; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) by A1, FUNCOP_1:62; ::_thesis: verum end; end; end; theorem :: FINSEQOP:32 for D being non empty set for d1, d2 being Element of D for i being Nat for T being Tuple of i,D for F being BinOp of D st F is associative holds F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) proof let D be non empty set ; ::_thesis: for d1, d2 being Element of D for i being Nat for T being Tuple of i,D for F being BinOp of D st F is associative holds F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) let d1, d2 be Element of D; ::_thesis: for i being Nat for T being Tuple of i,D for F being BinOp of D st F is associative holds F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) let i be Nat; ::_thesis: for T being Tuple of i,D for F being BinOp of D st F is associative holds F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative holds F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) let F be BinOp of D; ::_thesis: ( F is associative implies F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) ) assume A1: F is associative ; ::_thesis: F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) then ( T = <*> D & F [:] (T,d1) = <*> D ) by Lm3; hence F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) ; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) by A1, FUNCOP_1:63; ::_thesis: verum end; end; end; theorem :: FINSEQOP:33 for D being non empty set for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is commutative holds F .: (T1,T2) = F .: (T2,T1) proof let D be non empty set ; ::_thesis: for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is commutative holds F .: (T1,T2) = F .: (T2,T1) let i be Nat; ::_thesis: for T1, T2 being Tuple of i,D for F being BinOp of D st F is commutative holds F .: (T1,T2) = F .: (T2,T1) let T1, T2 be Tuple of i,D; ::_thesis: for F being BinOp of D st F is commutative holds F .: (T1,T2) = F .: (T2,T1) let F be BinOp of D; ::_thesis: ( F is commutative implies F .: (T1,T2) = F .: (T2,T1) ) assume A1: F is commutative ; ::_thesis: F .: (T1,T2) = F .: (T2,T1) percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: F .: (T1,T2) = F .: (T2,T1) then F .: (T1,T2) = <*> D by Lm1; hence F .: (T1,T2) = F .: (T2,T1) by A2, Lm1; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: F .: (T1,T2) = F .: (T2,T1) then reconsider C = Seg i as non empty set ; ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4; hence F .: (T1,T2) = F .: (T2,T1) by A1, FUNCOP_1:65; ::_thesis: verum end; end; end; theorem :: FINSEQOP:34 for D being non empty set for d being Element of D for i being Nat for T being Tuple of i,D for F being BinOp of D st F is commutative holds F [;] (d,T) = F [:] (T,d) proof let D be non empty set ; ::_thesis: for d being Element of D for i being Nat for T being Tuple of i,D for F being BinOp of D st F is commutative holds F [;] (d,T) = F [:] (T,d) let d be Element of D; ::_thesis: for i being Nat for T being Tuple of i,D for F being BinOp of D st F is commutative holds F [;] (d,T) = F [:] (T,d) let i be Nat; ::_thesis: for T being Tuple of i,D for F being BinOp of D st F is commutative holds F [;] (d,T) = F [:] (T,d) let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is commutative holds F [;] (d,T) = F [:] (T,d) let F be BinOp of D; ::_thesis: ( F is commutative implies F [;] (d,T) = F [:] (T,d) ) assume A1: F is commutative ; ::_thesis: F [;] (d,T) = F [:] (T,d) percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: F [;] (d,T) = F [:] (T,d) then F [;] (d,T) = <*> D by Lm2; hence F [;] (d,T) = F [:] (T,d) by A2, Lm3; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: F [;] (d,T) = F [:] (T,d) then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence F [;] (d,T) = F [:] (T,d) by A1, FUNCOP_1:64; ::_thesis: verum end; end; end; theorem Th35: :: FINSEQOP:35 for C, D being non empty set for d1, d2 being Element of D for f being Function of C,D for F, G being BinOp of D st F is_distributive_wrt G holds F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f))) proof let C, D be non empty set ; ::_thesis: for d1, d2 being Element of D for f being Function of C,D for F, G being BinOp of D st F is_distributive_wrt G holds F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f))) let d1, d2 be Element of D; ::_thesis: for f being Function of C,D for F, G being BinOp of D st F is_distributive_wrt G holds F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f))) let f be Function of C,D; ::_thesis: for F, G being BinOp of D st F is_distributive_wrt G holds F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f))) let F, G be BinOp of D; ::_thesis: ( F is_distributive_wrt G implies F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f))) ) assume A1: F is_distributive_wrt G ; ::_thesis: F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f))) now__::_thesis:_for_c_being_Element_of_C_holds_(F_[;]_((G_._(d1,d2)),f))_._c_=_(G_.:_((F_[;]_(d1,f)),(F_[;]_(d2,f))))_._c let c be Element of C; ::_thesis: (F [;] ((G . (d1,d2)),f)) . c = (G .: ((F [;] (d1,f)),(F [;] (d2,f)))) . 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 ; ::_thesis: verum end; hence F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f))) by FUNCT_2:63; ::_thesis: verum end; theorem Th36: :: FINSEQOP:36 for C, D being non empty set for d1, d2 being Element of D for f being Function of C,D for F, G being BinOp of D st F is_distributive_wrt G holds F [:] (f,(G . (d1,d2))) = G .: ((F [:] (f,d1)),(F [:] (f,d2))) proof let C, D be non empty set ; ::_thesis: for d1, d2 being Element of D for f being Function of C,D for F, G being BinOp of D st F is_distributive_wrt G holds F [:] (f,(G . (d1,d2))) = G .: ((F [:] (f,d1)),(F [:] (f,d2))) let d1, d2 be Element of D; ::_thesis: for f being Function of C,D for F, G being BinOp of D st F is_distributive_wrt G holds F [:] (f,(G . (d1,d2))) = G .: ((F [:] (f,d1)),(F [:] (f,d2))) let f be Function of C,D; ::_thesis: for F, G being BinOp of D st F is_distributive_wrt G holds F [:] (f,(G . (d1,d2))) = G .: ((F [:] (f,d1)),(F [:] (f,d2))) let F, G be BinOp of D; ::_thesis: ( F is_distributive_wrt G implies F [:] (f,(G . (d1,d2))) = G .: ((F [:] (f,d1)),(F [:] (f,d2))) ) assume A1: F is_distributive_wrt G ; ::_thesis: F [:] (f,(G . (d1,d2))) = G .: ((F [:] (f,d1)),(F [:] (f,d2))) now__::_thesis:_for_c_being_Element_of_C_holds_(F_[:]_(f,(G_._(d1,d2))))_._c_=_(G_.:_((F_[:]_(f,d1)),(F_[:]_(f,d2))))_._c let c be Element of C; ::_thesis: (F [:] (f,(G . (d1,d2)))) . c = (G .: ((F [:] (f,d1)),(F [:] (f,d2)))) . 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 ; ::_thesis: verum end; hence F [:] (f,(G . (d1,d2))) = G .: ((F [:] (f,d1)),(F [:] (f,d2))) by FUNCT_2:63; ::_thesis: verum end; theorem Th37: :: FINSEQOP:37 for C, E, D being non empty set for f, f9 being Function of C,D for h being Function of D,E for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F .: (f,f9)) = H .: ((h * f),(h * f9)) proof let C, E, D be non empty set ; ::_thesis: for f, f9 being Function of C,D for h being Function of D,E for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F .: (f,f9)) = H .: ((h * f),(h * f9)) let f, f9 be Function of C,D; ::_thesis: for h being Function of D,E for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F .: (f,f9)) = H .: ((h * f),(h * f9)) let h be Function of D,E; ::_thesis: for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F .: (f,f9)) = H .: ((h * f),(h * f9)) let F be BinOp of D; ::_thesis: for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F .: (f,f9)) = H .: ((h * f),(h * f9)) let H be BinOp of E; ::_thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F .: (f,f9)) = H .: ((h * f),(h * f9)) ) assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h * (F .: (f,f9)) = H .: ((h * f),(h * f9)) now__::_thesis:_for_c_being_Element_of_C_holds_(h_*_(F_.:_(f,f9)))_._c_=_(H_.:_((h_*_f),(h_*_f9)))_._c let c be Element of C; ::_thesis: (h * (F .: (f,f9))) . c = (H .: ((h * f),(h * f9))) . 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 ; ::_thesis: verum end; hence h * (F .: (f,f9)) = H .: ((h * f),(h * f9)) by FUNCT_2:63; ::_thesis: verum end; theorem Th38: :: FINSEQOP:38 for C, E, D being non empty set for d being Element of D for f being Function of C,D for h being Function of D,E for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,f)) = H [;] ((h . d),(h * f)) proof let C, E, D be non empty set ; ::_thesis: for d being Element of D for f being Function of C,D for h being Function of D,E for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,f)) = H [;] ((h . d),(h * f)) let d be Element of D; ::_thesis: for f being Function of C,D for h being Function of D,E for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,f)) = H [;] ((h . d),(h * f)) let f be Function of C,D; ::_thesis: for h being Function of D,E for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,f)) = H [;] ((h . d),(h * f)) let h be Function of D,E; ::_thesis: for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,f)) = H [;] ((h . d),(h * f)) let F be BinOp of D; ::_thesis: for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,f)) = H [;] ((h . d),(h * f)) let H be BinOp of E; ::_thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F [;] (d,f)) = H [;] ((h . d),(h * f)) ) assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h * (F [;] (d,f)) = H [;] ((h . d),(h * f)) 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 ; ::_thesis: verum end; theorem Th39: :: FINSEQOP:39 for C, E, D being non empty set for d being Element of D for f being Function of C,D for h being Function of D,E for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (f,d)) = H [:] ((h * f),(h . d)) proof let C, E, D be non empty set ; ::_thesis: for d being Element of D for f being Function of C,D for h being Function of D,E for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (f,d)) = H [:] ((h * f),(h . d)) let d be Element of D; ::_thesis: for f being Function of C,D for h being Function of D,E for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (f,d)) = H [:] ((h * f),(h . d)) let f be Function of C,D; ::_thesis: for h being Function of D,E for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (f,d)) = H [:] ((h * f),(h . d)) let h be Function of D,E; ::_thesis: for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (f,d)) = H [:] ((h * f),(h . d)) let F be BinOp of D; ::_thesis: for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (f,d)) = H [:] ((h * f),(h . d)) let H be BinOp of E; ::_thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F [:] (f,d)) = H [:] ((h * f),(h . d)) ) assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h * (F [:] (f,d)) = H [:] ((h * f),(h . d)) 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 ; ::_thesis: verum end; theorem :: FINSEQOP:40 for C, D being non empty set for f, f9 being Function of C,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F .: (f,f9)) = F .: ((u * f),(u * f9)) proof let C, D be non empty set ; ::_thesis: for f, f9 being Function of C,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F .: (f,f9)) = F .: ((u * f),(u * f9)) let f, f9 be Function of C,D; ::_thesis: for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F .: (f,f9)) = F .: ((u * f),(u * f9)) let F be BinOp of D; ::_thesis: for u being UnOp of D st u is_distributive_wrt F holds u * (F .: (f,f9)) = F .: ((u * f),(u * f9)) let u be UnOp of D; ::_thesis: ( u is_distributive_wrt F implies u * (F .: (f,f9)) = F .: ((u * f),(u * f9)) ) assume for d1, d2 being Element of D holds u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) ; :: according to BINOP_1:def_20 ::_thesis: u * (F .: (f,f9)) = F .: ((u * f),(u * f9)) hence u * (F .: (f,f9)) = F .: ((u * f),(u * f9)) by Th37; ::_thesis: verum end; theorem :: FINSEQOP:41 for C, D being non empty set for d being Element of D for f being Function of C,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [;] (d,f)) = F [;] ((u . d),(u * f)) proof let C, D be non empty set ; ::_thesis: for d being Element of D for f being Function of C,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [;] (d,f)) = F [;] ((u . d),(u * f)) let d be Element of D; ::_thesis: for f being Function of C,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [;] (d,f)) = F [;] ((u . d),(u * f)) let f be Function of C,D; ::_thesis: for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [;] (d,f)) = F [;] ((u . d),(u * f)) let F be BinOp of D; ::_thesis: for u being UnOp of D st u is_distributive_wrt F holds u * (F [;] (d,f)) = F [;] ((u . d),(u * f)) let u be UnOp of D; ::_thesis: ( u is_distributive_wrt F implies u * (F [;] (d,f)) = F [;] ((u . d),(u * f)) ) assume for d1, d2 being Element of D holds u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) ; :: according to BINOP_1:def_20 ::_thesis: u * (F [;] (d,f)) = F [;] ((u . d),(u * f)) hence u * (F [;] (d,f)) = F [;] ((u . d),(u * f)) by Th38; ::_thesis: verum end; theorem :: FINSEQOP:42 for C, D being non empty set for d being Element of D for f being Function of C,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [:] (f,d)) = F [:] ((u * f),(u . d)) proof let C, D be non empty set ; ::_thesis: for d being Element of D for f being Function of C,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [:] (f,d)) = F [:] ((u * f),(u . d)) let d be Element of D; ::_thesis: for f being Function of C,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [:] (f,d)) = F [:] ((u * f),(u . d)) let f be Function of C,D; ::_thesis: for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [:] (f,d)) = F [:] ((u * f),(u . d)) let F be BinOp of D; ::_thesis: for u being UnOp of D st u is_distributive_wrt F holds u * (F [:] (f,d)) = F [:] ((u * f),(u . d)) let u be UnOp of D; ::_thesis: ( u is_distributive_wrt F implies u * (F [:] (f,d)) = F [:] ((u * f),(u . d)) ) assume for d1, d2 being Element of D holds u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) ; :: according to BINOP_1:def_20 ::_thesis: u * (F [:] (f,d)) = F [:] ((u * f),(u . d)) hence u * (F [:] (f,d)) = F [:] ((u * f),(u . d)) by Th39; ::_thesis: verum end; theorem Th43: :: FINSEQOP:43 for D, C being non empty set for f being Function of C,D for F being BinOp of D st F is having_a_unity holds ( F .: ((C --> (the_unity_wrt F)),f) = f & F .: (f,(C --> (the_unity_wrt F))) = f ) proof let D, C be non empty set ; ::_thesis: for f being Function of C,D for F being BinOp of D st F is having_a_unity holds ( F .: ((C --> (the_unity_wrt F)),f) = f & F .: (f,(C --> (the_unity_wrt F))) = f ) let f be Function of C,D; ::_thesis: for F being BinOp of D st F is having_a_unity holds ( F .: ((C --> (the_unity_wrt F)),f) = f & F .: (f,(C --> (the_unity_wrt F))) = f ) let F be BinOp of D; ::_thesis: ( F is having_a_unity implies ( F .: ((C --> (the_unity_wrt F)),f) = f & F .: (f,(C --> (the_unity_wrt F))) = f ) ) set e = the_unity_wrt F; reconsider g = C --> (the_unity_wrt F) as Function of C,D ; assume A1: F is having_a_unity ; ::_thesis: ( F .: ((C --> (the_unity_wrt F)),f) = f & F .: (f,(C --> (the_unity_wrt F))) = f ) now__::_thesis:_for_c_being_Element_of_C_holds_(F_.:_(g,f))_._c_=_f_._c let c be Element of C; ::_thesis: (F .: (g,f)) . c = f . c thus (F .: (g,f)) . c = F . ((g . c),(f . c)) by FUNCOP_1:37 .= F . ((the_unity_wrt F),(f . c)) by FUNCOP_1:7 .= f . c by A1, SETWISEO:15 ; ::_thesis: verum end; hence F .: ((C --> (the_unity_wrt F)),f) = f by FUNCT_2:63; ::_thesis: F .: (f,(C --> (the_unity_wrt F))) = f now__::_thesis:_for_c_being_Element_of_C_holds_(F_.:_(f,g))_._c_=_f_._c let c be Element of C; ::_thesis: (F .: (f,g)) . c = f . c thus (F .: (f,g)) . c = F . ((f . c),(g . c)) by FUNCOP_1:37 .= F . ((f . c),(the_unity_wrt F)) by FUNCOP_1:7 .= f . c by A1, SETWISEO:15 ; ::_thesis: verum end; hence F .: (f,(C --> (the_unity_wrt F))) = f by FUNCT_2:63; ::_thesis: verum end; theorem Th44: :: FINSEQOP:44 for C, D being non empty set for f being Function of C,D for F being BinOp of D st F is having_a_unity holds F [;] ((the_unity_wrt F),f) = f proof let C, D be non empty set ; ::_thesis: for f being Function of C,D for F being BinOp of D st F is having_a_unity holds F [;] ((the_unity_wrt F),f) = f let f be Function of C,D; ::_thesis: for F being BinOp of D st F is having_a_unity holds F [;] ((the_unity_wrt F),f) = f let F be BinOp of D; ::_thesis: ( F is having_a_unity implies F [;] ((the_unity_wrt F),f) = f ) set e = the_unity_wrt F; assume A1: F is having_a_unity ; ::_thesis: F [;] ((the_unity_wrt F),f) = f now__::_thesis:_for_c_being_Element_of_C_holds_(F_[;]_((the_unity_wrt_F),f))_._c_=_f_._c let c be Element of C; ::_thesis: (F [;] ((the_unity_wrt F),f)) . c = f . c thus (F [;] ((the_unity_wrt F),f)) . c = F . ((the_unity_wrt F),(f . c)) by FUNCOP_1:53 .= f . c by A1, SETWISEO:15 ; ::_thesis: verum end; hence F [;] ((the_unity_wrt F),f) = f by FUNCT_2:63; ::_thesis: verum end; theorem Th45: :: FINSEQOP:45 for C, D being non empty set for f being Function of C,D for F being BinOp of D st F is having_a_unity holds F [:] (f,(the_unity_wrt F)) = f proof let C, D be non empty set ; ::_thesis: for f being Function of C,D for F being BinOp of D st F is having_a_unity holds F [:] (f,(the_unity_wrt F)) = f let f be Function of C,D; ::_thesis: for F being BinOp of D st F is having_a_unity holds F [:] (f,(the_unity_wrt F)) = f let F be BinOp of D; ::_thesis: ( F is having_a_unity implies F [:] (f,(the_unity_wrt F)) = f ) set e = the_unity_wrt F; assume A1: F is having_a_unity ; ::_thesis: F [:] (f,(the_unity_wrt F)) = f now__::_thesis:_for_c_being_Element_of_C_holds_(F_[:]_(f,(the_unity_wrt_F)))_._c_=_f_._c let c be Element of C; ::_thesis: (F [:] (f,(the_unity_wrt F))) . c = f . c thus (F [:] (f,(the_unity_wrt F))) . c = F . ((f . c),(the_unity_wrt F)) by FUNCOP_1:48 .= f . c by A1, SETWISEO:15 ; ::_thesis: verum end; hence F [:] (f,(the_unity_wrt F)) = f by FUNCT_2:63; ::_thesis: verum end; theorem :: FINSEQOP:46 for D being non empty set for d1, d2 being Element of D for i being Nat for T being Tuple of i,D for F, G being BinOp of D st F is_distributive_wrt G holds F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) proof let D be non empty set ; ::_thesis: for d1, d2 being Element of D for i being Nat for T being Tuple of i,D for F, G being BinOp of D st F is_distributive_wrt G holds F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) let d1, d2 be Element of D; ::_thesis: for i being Nat for T being Tuple of i,D for F, G being BinOp of D st F is_distributive_wrt G holds F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) let i be Nat; ::_thesis: for T being Tuple of i,D for F, G being BinOp of D st F is_distributive_wrt G holds F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) let T be Tuple of i,D; ::_thesis: for F, G being BinOp of D st F is_distributive_wrt G holds F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) let F, G be BinOp of D; ::_thesis: ( F is_distributive_wrt G implies F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) ) assume A1: F is_distributive_wrt G ; ::_thesis: F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) then ( F [;] (d1,T) = <*> D & F [;] ((G . (d1,d2)),T) = <*> D ) by Lm2; hence F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) by FINSEQ_2:73; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) by A1, Th35; ::_thesis: verum end; end; end; theorem :: FINSEQOP:47 for D being non empty set for d1, d2 being Element of D for i being Nat for T being Tuple of i,D for F, G being BinOp of D st F is_distributive_wrt G holds F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) proof let D be non empty set ; ::_thesis: for d1, d2 being Element of D for i being Nat for T being Tuple of i,D for F, G being BinOp of D st F is_distributive_wrt G holds F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) let d1, d2 be Element of D; ::_thesis: for i being Nat for T being Tuple of i,D for F, G being BinOp of D st F is_distributive_wrt G holds F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) let i be Nat; ::_thesis: for T being Tuple of i,D for F, G being BinOp of D st F is_distributive_wrt G holds F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) let T be Tuple of i,D; ::_thesis: for F, G being BinOp of D st F is_distributive_wrt G holds F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) let F, G be BinOp of D; ::_thesis: ( F is_distributive_wrt G implies F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) ) assume A1: F is_distributive_wrt G ; ::_thesis: F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) then ( F [:] (T,d1) = <*> D & F [:] (T,(G . (d1,d2))) = <*> D ) by Lm3; hence F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) by FINSEQ_2:73; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) by A1, Th36; ::_thesis: verum end; end; end; theorem Th48: :: FINSEQOP:48 for E, D being non empty set for i being Nat for h being Function of D,E for T1, T2 being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) proof let E, D be non empty set ; ::_thesis: for i being Nat for h being Function of D,E for T1, T2 being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) let i be Nat; ::_thesis: for h being Function of D,E for T1, T2 being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) let h be Function of D,E; ::_thesis: for T1, T2 being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) let T1, T2 be Tuple of i,D; ::_thesis: for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) let F be BinOp of D; ::_thesis: for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) let H be BinOp of E; ::_thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) ) assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) then F .: (T1,T2) = <*> D by Lm1; then A3: h * (F .: (T1,T2)) = <*> E ; h * T1 = <*> E by A2; hence h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) by A3, FINSEQ_2:73; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) then reconsider C = Seg i as non empty set ; ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4; hence h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) by A1, Th37; ::_thesis: verum end; end; end; theorem Th49: :: FINSEQOP:49 for E, D being non empty set for d being Element of D for i being Nat for h being Function of D,E for T being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) proof let E, D be non empty set ; ::_thesis: for d being Element of D for i being Nat for h being Function of D,E for T being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) let d be Element of D; ::_thesis: for i being Nat for h being Function of D,E for T being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) let i be Nat; ::_thesis: for h being Function of D,E for T being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) let h be Function of D,E; ::_thesis: for T being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) let T be Tuple of i,D; ::_thesis: for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) let F be BinOp of D; ::_thesis: for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) let H be BinOp of E; ::_thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) ) assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) then F [;] (d,T) = <*> D by Lm2; then A3: h * (F [;] (d,T)) = <*> E ; h * T = <*> E by A2; hence h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) by A3, FINSEQ_2:79; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) by A1, Th38; ::_thesis: verum end; end; end; theorem Th50: :: FINSEQOP:50 for E, D being non empty set for d being Element of D for i being Nat for h being Function of D,E for T being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) proof let E, D be non empty set ; ::_thesis: for d being Element of D for i being Nat for h being Function of D,E for T being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) let d be Element of D; ::_thesis: for i being Nat for h being Function of D,E for T being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) let i be Nat; ::_thesis: for h being Function of D,E for T being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) let h be Function of D,E; ::_thesis: for T being Tuple of i,D for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) let T be Tuple of i,D; ::_thesis: for F being BinOp of D for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) let F be BinOp of D; ::_thesis: for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) let H be BinOp of E; ::_thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) ) assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) then F [:] (T,d) = <*> D by Lm3; then A3: h * (F [:] (T,d)) = <*> E ; h * T = <*> E by A2; hence h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) by A3, FINSEQ_2:85; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) by A1, Th39; ::_thesis: verum end; end; end; theorem :: FINSEQOP:51 for D being non empty set for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2)) proof let D be non empty set ; ::_thesis: for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2)) let i be Nat; ::_thesis: for T1, T2 being Tuple of i,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2)) let T1, T2 be Tuple of i,D; ::_thesis: for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2)) let F be BinOp of D; ::_thesis: for u being UnOp of D st u is_distributive_wrt F holds u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2)) let u be UnOp of D; ::_thesis: ( u is_distributive_wrt F implies u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2)) ) assume for d1, d2 being Element of D holds u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) ; :: according to BINOP_1:def_20 ::_thesis: u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2)) hence u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2)) by Th48; ::_thesis: verum end; theorem :: FINSEQOP:52 for D being non empty set for d being Element of D for i being Nat for T being Tuple of i,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [;] (d,T)) = F [;] ((u . d),(u * T)) proof let D be non empty set ; ::_thesis: for d being Element of D for i being Nat for T being Tuple of i,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [;] (d,T)) = F [;] ((u . d),(u * T)) let d be Element of D; ::_thesis: for i being Nat for T being Tuple of i,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [;] (d,T)) = F [;] ((u . d),(u * T)) let i be Nat; ::_thesis: for T being Tuple of i,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [;] (d,T)) = F [;] ((u . d),(u * T)) let T be Tuple of i,D; ::_thesis: for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [;] (d,T)) = F [;] ((u . d),(u * T)) let F be BinOp of D; ::_thesis: for u being UnOp of D st u is_distributive_wrt F holds u * (F [;] (d,T)) = F [;] ((u . d),(u * T)) let u be UnOp of D; ::_thesis: ( u is_distributive_wrt F implies u * (F [;] (d,T)) = F [;] ((u . d),(u * T)) ) assume for d1, d2 being Element of D holds u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) ; :: according to BINOP_1:def_20 ::_thesis: u * (F [;] (d,T)) = F [;] ((u . d),(u * T)) hence u * (F [;] (d,T)) = F [;] ((u . d),(u * T)) by Th49; ::_thesis: verum end; theorem :: FINSEQOP:53 for D being non empty set for d being Element of D for i being Nat for T being Tuple of i,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [:] (T,d)) = F [:] ((u * T),(u . d)) proof let D be non empty set ; ::_thesis: for d being Element of D for i being Nat for T being Tuple of i,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [:] (T,d)) = F [:] ((u * T),(u . d)) let d be Element of D; ::_thesis: for i being Nat for T being Tuple of i,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [:] (T,d)) = F [:] ((u * T),(u . d)) let i be Nat; ::_thesis: for T being Tuple of i,D for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [:] (T,d)) = F [:] ((u * T),(u . d)) let T be Tuple of i,D; ::_thesis: for F being BinOp of D for u being UnOp of D st u is_distributive_wrt F holds u * (F [:] (T,d)) = F [:] ((u * T),(u . d)) let F be BinOp of D; ::_thesis: for u being UnOp of D st u is_distributive_wrt F holds u * (F [:] (T,d)) = F [:] ((u * T),(u . d)) let u be UnOp of D; ::_thesis: ( u is_distributive_wrt F implies u * (F [:] (T,d)) = F [:] ((u * T),(u . d)) ) assume for d1, d2 being Element of D holds u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) ; :: according to BINOP_1:def_20 ::_thesis: u * (F [:] (T,d)) = F [:] ((u * T),(u . d)) hence u * (F [:] (T,d)) = F [:] ((u * T),(u . d)) by Th50; ::_thesis: verum end; theorem :: FINSEQOP:54 for D being non empty set for d being Element of D for G, F being BinOp of D for u being UnOp of D st G is_distributive_wrt F & u = G [;] (d,(id D)) holds u is_distributive_wrt F proof let D be non empty set ; ::_thesis: for d being Element of D for G, F being BinOp of D for u being UnOp of D st G is_distributive_wrt F & u = G [;] (d,(id D)) holds u is_distributive_wrt F let d be Element of D; ::_thesis: for G, F being BinOp of D for u being UnOp of D st G is_distributive_wrt F & u = G [;] (d,(id D)) holds u is_distributive_wrt F let G, F be BinOp of D; ::_thesis: for u being UnOp of D st G is_distributive_wrt F & u = G [;] (d,(id D)) holds u is_distributive_wrt F let u be UnOp of D; ::_thesis: ( G is_distributive_wrt F & u = G [;] (d,(id D)) implies u is_distributive_wrt F ) assume that A1: G is_distributive_wrt F and A2: u = G [;] (d,(id D)) ; ::_thesis: u is_distributive_wrt F let d1 be Element of D; :: according to BINOP_1:def_20 ::_thesis: for b1 being Element of D holds u . (F . (d1,b1)) = F . ((u . d1),(u . b1)) let d2 be Element of D; ::_thesis: u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) thus u . (F . (d1,d2)) = G . (d,((id D) . (F . (d1,d2)))) by A2, FUNCOP_1:53 .= G . (d,(F . (d1,d2))) by FUNCT_1:18 .= F . ((G . (d,d1)),(G . (d,d2))) by A1, BINOP_1:11 .= F . ((G . (d,((id D) . d1))),(G . (d,d2))) by FUNCT_1:18 .= F . ((G . (d,((id D) . d1))),(G . (d,((id D) . d2)))) by FUNCT_1:18 .= F . ((u . d1),(G . (d,((id D) . d2)))) by A2, FUNCOP_1:53 .= F . ((u . d1),(u . d2)) by A2, FUNCOP_1:53 ; ::_thesis: verum end; theorem :: FINSEQOP:55 for D being non empty set for d being Element of D for G, F being BinOp of D for u being UnOp of D st G is_distributive_wrt F & u = G [:] ((id D),d) holds u is_distributive_wrt F proof let D be non empty set ; ::_thesis: for d being Element of D for G, F being BinOp of D for u being UnOp of D st G is_distributive_wrt F & u = G [:] ((id D),d) holds u is_distributive_wrt F let d be Element of D; ::_thesis: for G, F being BinOp of D for u being UnOp of D st G is_distributive_wrt F & u = G [:] ((id D),d) holds u is_distributive_wrt F let G, F be BinOp of D; ::_thesis: for u being UnOp of D st G is_distributive_wrt F & u = G [:] ((id D),d) holds u is_distributive_wrt F let u be UnOp of D; ::_thesis: ( G is_distributive_wrt F & u = G [:] ((id D),d) implies u is_distributive_wrt F ) assume that A1: G is_distributive_wrt F and A2: u = G [:] ((id D),d) ; ::_thesis: u is_distributive_wrt F let d1 be Element of D; :: according to BINOP_1:def_20 ::_thesis: for b1 being Element of D holds u . (F . (d1,b1)) = F . ((u . d1),(u . b1)) let d2 be Element of D; ::_thesis: u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) thus u . (F . (d1,d2)) = G . (((id D) . (F . (d1,d2))),d) by A2, FUNCOP_1:48 .= G . ((F . (d1,d2)),d) by FUNCT_1:18 .= F . ((G . (d1,d)),(G . (d2,d))) by A1, BINOP_1:11 .= F . ((G . (((id D) . d1),d)),(G . (d2,d))) by FUNCT_1:18 .= F . ((G . (((id D) . d1),d)),(G . (((id D) . d2),d))) by FUNCT_1:18 .= F . ((u . d1),(G . (((id D) . d2),d))) by A2, FUNCOP_1:48 .= F . ((u . d1),(u . d2)) by A2, FUNCOP_1:48 ; ::_thesis: verum end; theorem :: FINSEQOP:56 for D being non empty set for i being Nat for T being Tuple of i,D for F being BinOp of D st F is having_a_unity holds ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) proof let D be non empty set ; ::_thesis: for i being Nat for T being Tuple of i,D for F being BinOp of D st F is having_a_unity holds ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) let i be Nat; ::_thesis: for T being Tuple of i,D for F being BinOp of D st F is having_a_unity holds ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is having_a_unity holds ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) let F be BinOp of D; ::_thesis: ( F is having_a_unity implies ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) ) assume A1: F is having_a_unity ; ::_thesis: ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) then T = <*> D ; hence ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) by A2, Lm1; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) by A1, Th43; ::_thesis: verum end; end; end; theorem :: FINSEQOP:57 for D being non empty set for i being Nat for T being Tuple of i,D for F being BinOp of D st F is having_a_unity holds F [;] ((the_unity_wrt F),T) = T proof let D be non empty set ; ::_thesis: for i being Nat for T being Tuple of i,D for F being BinOp of D st F is having_a_unity holds F [;] ((the_unity_wrt F),T) = T let i be Nat; ::_thesis: for T being Tuple of i,D for F being BinOp of D st F is having_a_unity holds F [;] ((the_unity_wrt F),T) = T let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is having_a_unity holds F [;] ((the_unity_wrt F),T) = T let F be BinOp of D; ::_thesis: ( F is having_a_unity implies F [;] ((the_unity_wrt F),T) = T ) assume A1: F is having_a_unity ; ::_thesis: F [;] ((the_unity_wrt F),T) = T percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: F [;] ((the_unity_wrt F),T) = T then T = <*> D ; hence F [;] ((the_unity_wrt F),T) = T by Lm2; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: F [;] ((the_unity_wrt F),T) = T then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence F [;] ((the_unity_wrt F),T) = T by A1, Th44; ::_thesis: verum end; end; end; theorem :: FINSEQOP:58 for D being non empty set for i being Nat for T being Tuple of i,D for F being BinOp of D st F is having_a_unity holds F [:] (T,(the_unity_wrt F)) = T proof let D be non empty set ; ::_thesis: for i being Nat for T being Tuple of i,D for F being BinOp of D st F is having_a_unity holds F [:] (T,(the_unity_wrt F)) = T let i be Nat; ::_thesis: for T being Tuple of i,D for F being BinOp of D st F is having_a_unity holds F [:] (T,(the_unity_wrt F)) = T let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is having_a_unity holds F [:] (T,(the_unity_wrt F)) = T let F be BinOp of D; ::_thesis: ( F is having_a_unity implies F [:] (T,(the_unity_wrt F)) = T ) assume A1: F is having_a_unity ; ::_thesis: F [:] (T,(the_unity_wrt F)) = T percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: F [:] (T,(the_unity_wrt F)) = T then T = <*> D ; hence F [:] (T,(the_unity_wrt F)) = T by Lm3; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: F [:] (T,(the_unity_wrt F)) = T then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence F [:] (T,(the_unity_wrt F)) = T by A1, Th45; ::_thesis: verum end; end; end; definition let D be non empty set ; let u be UnOp of D; let F be BinOp of D; predu is_an_inverseOp_wrt F means :Def1: :: FINSEQOP:def 1 for d being Element of D holds ( F . (d,(u . d)) = the_unity_wrt F & F . ((u . d),d) = the_unity_wrt F ); end; :: deftheorem Def1 defines is_an_inverseOp_wrt FINSEQOP:def_1_:_ for D being non empty set for u being UnOp of D for F being BinOp of D holds ( u is_an_inverseOp_wrt F iff for d being Element of D holds ( F . (d,(u . d)) = the_unity_wrt F & F . ((u . d),d) = the_unity_wrt F ) ); definition let D be non empty set ; let F be BinOp of D; attrF is having_an_inverseOp means :Def2: :: FINSEQOP:def 2 ex u being UnOp of D st u is_an_inverseOp_wrt F; end; :: deftheorem Def2 defines having_an_inverseOp FINSEQOP:def_2_:_ for D being non empty set for F being BinOp of D holds ( F is having_an_inverseOp iff ex u being UnOp of D st u is_an_inverseOp_wrt F ); definition let D be non empty set ; let F be BinOp of D; 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: :: FINSEQOP:def 3 it is_an_inverseOp_wrt F; existence ex b1 being UnOp of D st b1 is_an_inverseOp_wrt F by A3, Def2; uniqueness for b1, b2 being UnOp of D st b1 is_an_inverseOp_wrt F & b2 is_an_inverseOp_wrt F holds b1 = b2 proof set e = the_unity_wrt F; let u1, u2 be UnOp of D; ::_thesis: ( u1 is_an_inverseOp_wrt F & u2 is_an_inverseOp_wrt F implies u1 = u2 ) assume that A4: for d being Element of D holds ( F . (d,(u1 . d)) = the_unity_wrt F & F . ((u1 . d),d) = the_unity_wrt F ) and A5: for d being Element of D holds ( F . (d,(u2 . d)) = the_unity_wrt F & F . ((u2 . d),d) = the_unity_wrt F ) ; :: according to FINSEQOP:def_1 ::_thesis: u1 = u2 now__::_thesis:_for_d_being_Element_of_D_holds_u1_._d_=_u2_._d let d be Element of D; ::_thesis: u1 . d = u2 . d set d1 = u1 . d; set d2 = u2 . d; thus u1 . d = F . ((u1 . d),(the_unity_wrt F)) by A1, SETWISEO:15 .= F . ((u1 . d),(F . (d,(u2 . d)))) by A5 .= F . ((F . ((u1 . d),d)),(u2 . d)) by A2, BINOP_1:def_3 .= F . ((the_unity_wrt F),(u2 . d)) by A4 .= u2 . d by A1, SETWISEO:15 ; ::_thesis: verum end; hence u1 = u2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def3 defines the_inverseOp_wrt FINSEQOP:def_3_:_ for D being non empty set for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds for b3 being UnOp of D holds ( b3 = the_inverseOp_wrt F iff b3 is_an_inverseOp_wrt F ); theorem Th59: :: FINSEQOP:59 for D being non empty set for d being Element of D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F ) proof let D be non empty set ; ::_thesis: for d being Element of D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F ) let d be Element of D; ::_thesis: for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F ) let F be BinOp of D; ::_thesis: ( 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 ) ) assume ( F is having_a_unity & F is associative & F is having_an_inverseOp ) ; ::_thesis: ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F ) then the_inverseOp_wrt F is_an_inverseOp_wrt F by Def3; hence ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F ) by Def1; ::_thesis: verum end; theorem Th60: :: FINSEQOP:60 for D being non empty set for d1, d2 being Element of D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & F . (d1,d2) = the_unity_wrt F holds ( d1 = (the_inverseOp_wrt F) . d2 & (the_inverseOp_wrt F) . d1 = d2 ) proof let D be non empty set ; ::_thesis: for d1, d2 being Element of D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & F . (d1,d2) = the_unity_wrt F holds ( d1 = (the_inverseOp_wrt F) . d2 & (the_inverseOp_wrt F) . d1 = d2 ) let d1, d2 be Element of D; ::_thesis: for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & F . (d1,d2) = the_unity_wrt F holds ( d1 = (the_inverseOp_wrt F) . d2 & (the_inverseOp_wrt F) . d1 = d2 ) let F be BinOp of D; ::_thesis: ( 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 ) ) 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 ; ::_thesis: ( d1 = (the_inverseOp_wrt F) . d2 & (the_inverseOp_wrt F) . d1 = d2 ) set e = the_unity_wrt F; set d3 = (the_inverseOp_wrt F) . d2; F . ((F . (d1,d2)),((the_inverseOp_wrt F) . d2)) = (the_inverseOp_wrt F) . d2 by A1, A4, SETWISEO:15; then F . (d1,(F . (d2,((the_inverseOp_wrt F) . d2)))) = (the_inverseOp_wrt F) . d2 by A2, BINOP_1:def_3; then F . (d1,(the_unity_wrt F)) = (the_inverseOp_wrt F) . d2 by A1, A2, A3, Th59; hence d1 = (the_inverseOp_wrt F) . d2 by A1, SETWISEO:15; ::_thesis: (the_inverseOp_wrt F) . d1 = d2 set d3 = (the_inverseOp_wrt F) . d1; F . (((the_inverseOp_wrt F) . d1),(F . (d1,d2))) = (the_inverseOp_wrt F) . d1 by A1, A4, SETWISEO:15; then F . ((F . (((the_inverseOp_wrt F) . d1),d1)),d2) = (the_inverseOp_wrt F) . d1 by A2, BINOP_1:def_3; then F . ((the_unity_wrt F),d2) = (the_inverseOp_wrt F) . d1 by A1, A2, A3, Th59; hence (the_inverseOp_wrt F) . d1 = d2 by A1, SETWISEO:15; ::_thesis: verum end; theorem Th61: :: FINSEQOP:61 for D being non empty set for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds (the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F proof let D be non empty set ; ::_thesis: for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds (the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F let F be BinOp of D; ::_thesis: ( 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 ) assume that A1: F is having_a_unity and A2: ( F is associative & F is having_an_inverseOp ) ; ::_thesis: (the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F set e = the_unity_wrt F; F . ((the_unity_wrt F),(the_unity_wrt F)) = the_unity_wrt F by A1, SETWISEO:15; hence (the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F by A1, A2, Th60; ::_thesis: verum end; theorem Th62: :: FINSEQOP:62 for D being non empty set for d being Element of D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds (the_inverseOp_wrt F) . ((the_inverseOp_wrt F) . d) = d proof let D be non empty set ; ::_thesis: for d being Element of D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds (the_inverseOp_wrt F) . ((the_inverseOp_wrt F) . d) = d let d be Element of D; ::_thesis: for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds (the_inverseOp_wrt F) . ((the_inverseOp_wrt F) . d) = d let F be BinOp of D; ::_thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp implies (the_inverseOp_wrt F) . ((the_inverseOp_wrt F) . d) = d ) assume A1: ( F is having_a_unity & F is associative & F is having_an_inverseOp ) ; ::_thesis: (the_inverseOp_wrt F) . ((the_inverseOp_wrt F) . d) = d then F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F by Th59; hence (the_inverseOp_wrt F) . ((the_inverseOp_wrt F) . d) = d by A1, Th60; ::_thesis: verum end; theorem Th63: :: FINSEQOP:63 for D being non empty set for F being BinOp of D st F is having_a_unity & F is associative & F is commutative & F is having_an_inverseOp holds the_inverseOp_wrt F is_distributive_wrt F proof let D be non empty set ; ::_thesis: for F being BinOp of D st F is having_a_unity & F is associative & F is commutative & F is having_an_inverseOp holds the_inverseOp_wrt F is_distributive_wrt F let F be BinOp of D; ::_thesis: ( 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 ) 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 ; ::_thesis: the_inverseOp_wrt F is_distributive_wrt F let d1 be Element of D; :: according to BINOP_1:def_20 ::_thesis: for b1 being Element of D holds (the_inverseOp_wrt F) . (F . (d1,b1)) = F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . b1)) let d2 be Element of D; ::_thesis: (the_inverseOp_wrt F) . (F . (d1,d2)) = F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . d2)) set e = the_unity_wrt F; set u = the_inverseOp_wrt F; F . ((F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . d2))),(F . (d1,d2))) = F . (((the_inverseOp_wrt F) . d1),(F . (((the_inverseOp_wrt F) . d2),(F . (d1,d2))))) by A2, BINOP_1:def_3 .= F . (((the_inverseOp_wrt F) . d1),(F . ((F . (((the_inverseOp_wrt F) . d2),d1)),d2))) by A2, BINOP_1:def_3 .= F . (((the_inverseOp_wrt F) . d1),(F . ((F . (d1,((the_inverseOp_wrt F) . d2))),d2))) by A3, BINOP_1:def_2 .= F . (((the_inverseOp_wrt F) . d1),(F . (d1,(F . (((the_inverseOp_wrt F) . d2),d2))))) by A2, BINOP_1:def_3 .= F . (((the_inverseOp_wrt F) . d1),(F . (d1,(the_unity_wrt F)))) by A1, A2, A4, Th59 .= F . ((F . (((the_inverseOp_wrt F) . d1),d1)),(the_unity_wrt F)) by A2, BINOP_1:def_3 .= F . ((the_unity_wrt F),(the_unity_wrt F)) by A1, A2, A4, Th59 .= the_unity_wrt F by A1, SETWISEO:15 ; hence (the_inverseOp_wrt F) . (F . (d1,d2)) = F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . d2)) by A1, A2, A4, Th60; ::_thesis: verum end; theorem Th64: :: FINSEQOP:64 for D being non empty set for d, d1, d2 being Element of D for F being BinOp of D st 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) ) holds d1 = d2 proof let D be non empty set ; ::_thesis: for d, d1, d2 being Element of D for F being BinOp of D st 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) ) holds d1 = d2 let d, d1, d2 be Element of D; ::_thesis: for F being BinOp of D st 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) ) holds d1 = d2 let F be BinOp of D; ::_thesis: ( 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 ) 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) ) ; ::_thesis: d1 = d2 set e = the_unity_wrt F; set u = the_inverseOp_wrt F; percases ( F . (d,d1) = F . (d,d2) or F . (d1,d) = F . (d2,d) ) by A4; supposeA5: F . (d,d1) = F . (d,d2) ; ::_thesis: d1 = d2 thus d1 = F . ((the_unity_wrt F),d1) by A1, SETWISEO:15 .= F . ((F . (((the_inverseOp_wrt F) . d),d)),d1) by A1, A2, A3, Th59 .= F . (((the_inverseOp_wrt F) . d),(F . (d,d2))) by A2, A5, BINOP_1:def_3 .= F . ((F . (((the_inverseOp_wrt F) . d),d)),d2) by A2, BINOP_1:def_3 .= F . ((the_unity_wrt F),d2) by A1, A2, A3, Th59 .= d2 by A1, SETWISEO:15 ; ::_thesis: verum end; supposeA6: F . (d1,d) = F . (d2,d) ; ::_thesis: d1 = d2 thus d1 = F . (d1,(the_unity_wrt F)) by A1, SETWISEO:15 .= F . (d1,(F . (d,((the_inverseOp_wrt F) . d)))) by A1, A2, A3, Th59 .= F . ((F . (d2,d)),((the_inverseOp_wrt F) . d)) by A2, A6, BINOP_1:def_3 .= F . (d2,(F . (d,((the_inverseOp_wrt F) . d)))) by A2, BINOP_1:def_3 .= F . (d2,(the_unity_wrt F)) by A1, A2, A3, Th59 .= d2 by A1, SETWISEO:15 ; ::_thesis: verum end; end; end; theorem Th65: :: FINSEQOP:65 for D being non empty set for d1, d2 being Element of D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & ( F . (d1,d2) = d2 or F . (d2,d1) = d2 ) holds d1 = the_unity_wrt F proof let D be non empty set ; ::_thesis: for d1, d2 being Element of D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & ( F . (d1,d2) = d2 or F . (d2,d1) = d2 ) holds d1 = the_unity_wrt F let d1, d2 be Element of D; ::_thesis: for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & ( F . (d1,d2) = d2 or F . (d2,d1) = d2 ) holds d1 = the_unity_wrt F let F be BinOp of D; ::_thesis: ( 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 ) assume that A1: F is having_a_unity and A2: ( F is associative & F is having_an_inverseOp ) ; ::_thesis: ( ( not F . (d1,d2) = d2 & not F . (d2,d1) = d2 ) or d1 = the_unity_wrt F ) set e = the_unity_wrt F; assume ( F . (d1,d2) = d2 or F . (d2,d1) = d2 ) ; ::_thesis: d1 = the_unity_wrt F then ( F . (d1,d2) = F . ((the_unity_wrt F),d2) or F . (d2,d1) = F . (d2,(the_unity_wrt F)) ) by A1, SETWISEO:15; hence d1 = the_unity_wrt F by A1, A2, Th64; ::_thesis: verum end; theorem Th66: :: FINSEQOP:66 for D being non empty set for e being Element of D for F, G being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F & e = the_unity_wrt F holds for d being Element of D holds ( G . (e,d) = e & G . (d,e) = e ) proof let D be non empty set ; ::_thesis: for e being Element of D for F, G being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F & e = the_unity_wrt F holds for d being Element of D holds ( G . (e,d) = e & G . (d,e) = e ) let e be Element of D; ::_thesis: for F, G being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F & e = the_unity_wrt F holds for d being Element of D holds ( G . (e,d) = e & G . (d,e) = e ) let F, G be BinOp of D; ::_thesis: ( 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 being Element of D holds ( G . (e,d) = e & G . (d,e) = e ) ) 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 ; ::_thesis: for d being Element of D holds ( G . (e,d) = e & G . (d,e) = e ) let d be Element of D; ::_thesis: ( G . (e,d) = e & G . (d,e) = e ) set ed = G . (e,d); F . ((G . (e,d)),(G . (e,d))) = G . ((F . (e,e)),d) by A4, BINOP_1:11 .= G . (e,d) by A2, A5, SETWISEO:15 ; hence G . (e,d) = e by A1, A2, A3, A5, Th65; ::_thesis: G . (d,e) = e set de = G . (d,e); F . ((G . (d,e)),(G . (d,e))) = G . (d,(F . (e,e))) by A4, BINOP_1:11 .= G . (d,e) by A2, A5, SETWISEO:15 ; hence G . (d,e) = e by A1, A2, A3, A5, Th65; ::_thesis: verum end; theorem Th67: :: FINSEQOP:67 for D being non empty set for d1, d2 being Element of D for F, G being BinOp of D for u being UnOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F holds ( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) ) proof let D be non empty set ; ::_thesis: for d1, d2 being Element of D for F, G being BinOp of D for u being UnOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F holds ( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) ) let d1, d2 be Element of D; ::_thesis: for F, G being BinOp of D for u being UnOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F holds ( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) ) let F, G be BinOp of D; ::_thesis: for u being UnOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F holds ( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) ) let u be UnOp of D; ::_thesis: ( 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)) ) ) 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 ; ::_thesis: ( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) ) 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 . ((the_unity_wrt F),d2) by A1, A2, Th59 .= the_unity_wrt F by A1, A3, Th66 ; hence u . (G . (d1,d2)) = G . ((u . d1),d2) by A1, A2, Th60; ::_thesis: u . (G . (d1,d2)) = G . (d1,(u . d2)) F . ((G . (d1,d2)),(G . (d1,(u . d2)))) = G . (d1,(F . (d2,(u . d2)))) by A3, BINOP_1:11 .= G . (d1,(the_unity_wrt F)) by A1, A2, Th59 .= the_unity_wrt F by A1, A3, Th66 ; hence u . (G . (d1,d2)) = G . (d1,(u . d2)) by A1, A2, Th60; ::_thesis: verum end; theorem :: FINSEQOP:68 for D being non empty set for F, G being BinOp of D for u being UnOp of D st 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 holds G [;] ((u . (the_unity_wrt G)),(id D)) = u proof let D be non empty set ; ::_thesis: for F, G being BinOp of D for u being UnOp of D st 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 holds G [;] ((u . (the_unity_wrt G)),(id D)) = u let F, G be BinOp of D; ::_thesis: for u being UnOp of D st 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 holds G [;] ((u . (the_unity_wrt G)),(id D)) = u let u be UnOp of D; ::_thesis: ( 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 ) 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 ; ::_thesis: G [;] ((u . (the_unity_wrt G)),(id D)) = u set o = the_unity_wrt G; for d being Element of D holds (G [;] ((u . (the_unity_wrt G)),(id D))) . d = u . d proof let d be Element of D; ::_thesis: (G [;] ((u . (the_unity_wrt G)),(id D))) . d = u . d thus (G [;] ((u . (the_unity_wrt G)),(id D))) . d = G . ((u . (the_unity_wrt G)),((id D) . d)) by FUNCOP_1:53 .= G . ((u . (the_unity_wrt G)),d) by FUNCT_1:18 .= u . (G . ((the_unity_wrt G),d)) by A1, Th67 .= u . d by A2, SETWISEO:15 ; ::_thesis: verum end; hence G [;] ((u . (the_unity_wrt G)),(id D)) = u by FUNCT_2:63; ::_thesis: verum end; theorem :: FINSEQOP:69 for D being non empty set for d being Element of D for F, G being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds (G [;] (d,(id D))) . (the_unity_wrt F) = the_unity_wrt F proof let D be non empty set ; ::_thesis: for d being Element of D for F, G being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds (G [;] (d,(id D))) . (the_unity_wrt F) = the_unity_wrt F let d be Element of D; ::_thesis: for F, G being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds (G [;] (d,(id D))) . (the_unity_wrt F) = the_unity_wrt F let F, G be BinOp of D; ::_thesis: ( 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 ) 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 ; ::_thesis: (G [;] (d,(id D))) . (the_unity_wrt F) = the_unity_wrt F set e = the_unity_wrt F; set i = the_inverseOp_wrt F; G . (d,(the_unity_wrt F)) = G . (d,(F . ((the_unity_wrt F),(the_unity_wrt F)))) by A2, SETWISEO:15 .= F . ((G . (d,(the_unity_wrt F))),(G . (d,(the_unity_wrt F)))) by A4, BINOP_1:11 ; then the_unity_wrt F = F . ((F . ((G . (d,(the_unity_wrt F))),(G . (d,(the_unity_wrt F))))),((the_inverseOp_wrt F) . (G . (d,(the_unity_wrt F))))) by A1, A2, A3, Th59; then the_unity_wrt F = F . ((G . (d,(the_unity_wrt F))),(F . ((G . (d,(the_unity_wrt F))),((the_inverseOp_wrt F) . (G . (d,(the_unity_wrt F))))))) by A1, BINOP_1:def_3; then the_unity_wrt F = F . ((G . (d,(the_unity_wrt F))),(the_unity_wrt F)) by A1, A2, A3, Th59; then the_unity_wrt F = G . (d,(the_unity_wrt F)) by A2, SETWISEO:15; then G . (d,((id D) . (the_unity_wrt F))) = the_unity_wrt F by FUNCT_1:18; hence (G [;] (d,(id D))) . (the_unity_wrt F) = the_unity_wrt F by FUNCOP_1:53; ::_thesis: verum end; theorem :: FINSEQOP:70 for D being non empty set for d being Element of D for F, G being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds (G [:] ((id D),d)) . (the_unity_wrt F) = the_unity_wrt F proof let D be non empty set ; ::_thesis: for d being Element of D for F, G being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds (G [:] ((id D),d)) . (the_unity_wrt F) = the_unity_wrt F let d be Element of D; ::_thesis: for F, G being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds (G [:] ((id D),d)) . (the_unity_wrt F) = the_unity_wrt F let F, G be BinOp of D; ::_thesis: ( 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 ) 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 ; ::_thesis: (G [:] ((id D),d)) . (the_unity_wrt F) = the_unity_wrt F set e = the_unity_wrt F; set i = the_inverseOp_wrt F; G . ((the_unity_wrt F),d) = G . ((F . ((the_unity_wrt F),(the_unity_wrt F))),d) by A2, SETWISEO:15 .= F . ((G . ((the_unity_wrt F),d)),(G . ((the_unity_wrt F),d))) by A4, BINOP_1:11 ; then the_unity_wrt F = F . ((F . ((G . ((the_unity_wrt F),d)),(G . ((the_unity_wrt F),d)))),((the_inverseOp_wrt F) . (G . ((the_unity_wrt F),d)))) by A1, A2, A3, Th59; then the_unity_wrt F = F . ((G . ((the_unity_wrt F),d)),(F . ((G . ((the_unity_wrt F),d)),((the_inverseOp_wrt F) . (G . ((the_unity_wrt F),d)))))) by A1, BINOP_1:def_3; then the_unity_wrt F = F . ((G . ((the_unity_wrt F),d)),(the_unity_wrt F)) by A1, A2, A3, Th59; then the_unity_wrt F = G . ((the_unity_wrt F),d) by A2, SETWISEO:15; then G . (((id D) . (the_unity_wrt F)),d) = the_unity_wrt F by FUNCT_1:18; hence (G [:] ((id D),d)) . (the_unity_wrt F) = the_unity_wrt F by FUNCOP_1:48; ::_thesis: verum end; theorem Th71: :: FINSEQOP:71 for D, C being non empty set for f being Function of C,D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds ( 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 let D, C be non empty set ; ::_thesis: for f being Function of C,D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds ( F .: (f,((the_inverseOp_wrt F) * f)) = C --> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * f),f) = C --> (the_unity_wrt F) ) let f be Function of C,D; ::_thesis: for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds ( F .: (f,((the_inverseOp_wrt F) * f)) = C --> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * f),f) = C --> (the_unity_wrt F) ) let F be BinOp of D; ::_thesis: ( 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) ) ) 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 ) ; ::_thesis: ( F .: (f,((the_inverseOp_wrt F) * f)) = C --> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * f),f) = C --> (the_unity_wrt F) ) now__::_thesis:_for_c_being_Element_of_C_holds_(F_.:_(f,((the_inverseOp_wrt_F)_*_f)))_._c_=_g_._c let c be Element of C; ::_thesis: (F .: (f,((the_inverseOp_wrt F) * f))) . c = g . c thus (F .: (f,((the_inverseOp_wrt F) * f))) . c = F . ((f . c),(((the_inverseOp_wrt F) * f) . c)) by FUNCOP_1:37 .= F . ((f . c),((the_inverseOp_wrt F) . (f . c))) by FUNCT_2:15 .= the_unity_wrt F by A1, Th59 .= g . c by FUNCOP_1:7 ; ::_thesis: verum end; hence F .: (f,((the_inverseOp_wrt F) * f)) = C --> (the_unity_wrt F) by FUNCT_2:63; ::_thesis: F .: (((the_inverseOp_wrt F) * f),f) = C --> (the_unity_wrt F) now__::_thesis:_for_c_being_Element_of_C_holds_(F_.:_(((the_inverseOp_wrt_F)_*_f),f))_._c_=_g_._c let c be Element of C; ::_thesis: (F .: (((the_inverseOp_wrt F) * f),f)) . c = g . c thus (F .: (((the_inverseOp_wrt F) * f),f)) . c = F . ((((the_inverseOp_wrt F) * f) . c),(f . c)) by FUNCOP_1:37 .= F . (((the_inverseOp_wrt F) . (f . c)),(f . c)) by FUNCT_2:15 .= the_unity_wrt F by A1, Th59 .= g . c by FUNCOP_1:7 ; ::_thesis: verum end; hence F .: (((the_inverseOp_wrt F) * f),f) = C --> (the_unity_wrt F) by FUNCT_2:63; ::_thesis: verum end; theorem Th72: :: FINSEQOP:72 for D, C being non empty set for f, f9 being Function of C,D for F being BinOp of D st F is associative & F is having_an_inverseOp & F is having_a_unity & F .: (f,f9) = C --> (the_unity_wrt F) holds ( f = (the_inverseOp_wrt F) * f9 & (the_inverseOp_wrt F) * f = f9 ) proof let D, C be non empty set ; ::_thesis: for f, f9 being Function of C,D for F being BinOp of D st F is associative & F is having_an_inverseOp & F is having_a_unity & F .: (f,f9) = C --> (the_unity_wrt F) holds ( f = (the_inverseOp_wrt F) * f9 & (the_inverseOp_wrt F) * f = f9 ) let f, f9 be Function of C,D; ::_thesis: for F being BinOp of D st F is associative & F is having_an_inverseOp & F is having_a_unity & F .: (f,f9) = C --> (the_unity_wrt F) holds ( f = (the_inverseOp_wrt F) * f9 & (the_inverseOp_wrt F) * f = f9 ) let F be BinOp of D; ::_thesis: ( 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 ) ) 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) ; ::_thesis: ( f = (the_inverseOp_wrt F) * f9 & (the_inverseOp_wrt F) * f = f9 ) set u = the_inverseOp_wrt F; set e = the_unity_wrt F; reconsider g = C --> (the_unity_wrt F) as Function of C,D ; now__::_thesis:_for_c_being_Element_of_C_holds_f_._c_=_((the_inverseOp_wrt_F)_*_f9)_._c let c be Element of C; ::_thesis: f . c = ((the_inverseOp_wrt F) * f9) . c F . ((f . c),(f9 . c)) = g . c by A2, FUNCOP_1:37 .= the_unity_wrt F by FUNCOP_1:7 ; hence f . c = (the_inverseOp_wrt F) . (f9 . c) by A1, Th60 .= ((the_inverseOp_wrt F) * f9) . c by FUNCT_2:15 ; ::_thesis: verum end; hence f = (the_inverseOp_wrt F) * f9 by FUNCT_2:63; ::_thesis: (the_inverseOp_wrt F) * f = f9 now__::_thesis:_for_c_being_Element_of_C_holds_((the_inverseOp_wrt_F)_*_f)_._c_=_f9_._c let c be Element of C; ::_thesis: ((the_inverseOp_wrt F) * f) . c = f9 . c F . ((f . c),(f9 . c)) = g . c by A2, FUNCOP_1:37 .= the_unity_wrt F by FUNCOP_1:7 ; then f9 . c = (the_inverseOp_wrt F) . (f . c) by A1, Th60; hence ((the_inverseOp_wrt F) * f) . c = f9 . c by FUNCT_2:15; ::_thesis: verum end; hence (the_inverseOp_wrt F) * f = f9 by FUNCT_2:63; ::_thesis: verum end; theorem :: FINSEQOP:73 for D being non empty set for i being Nat for T being Tuple of i,D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds ( 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 let D be non empty set ; ::_thesis: for i being Nat for T being Tuple of i,D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) ) let i be Nat; ::_thesis: for T being Tuple of i,D for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) ) let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) ) let F be BinOp of D; ::_thesis: ( 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) ) ) assume A1: ( F is having_a_unity & F is associative & F is having_an_inverseOp ) ; ::_thesis: ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) ) reconsider uT = (the_inverseOp_wrt F) * T as Element of i -tuples_on D by FINSEQ_2:113; percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) ) then ( F .: (T,uT) = <*> D & F .: (uT,T) = <*> D ) by Lm1; hence ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) ) by A2; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) ) then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) ) by A1, Th71; ::_thesis: verum end; end; end; theorem :: FINSEQOP:74 for D being non empty set for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative & F is having_an_inverseOp & F is having_a_unity & F .: (T1,T2) = i |-> (the_unity_wrt F) holds ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 ) proof let D be non empty set ; ::_thesis: for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative & F is having_an_inverseOp & F is having_a_unity & F .: (T1,T2) = i |-> (the_unity_wrt F) holds ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 ) let i be Nat; ::_thesis: for T1, T2 being Tuple of i,D for F being BinOp of D st F is associative & F is having_an_inverseOp & F is having_a_unity & F .: (T1,T2) = i |-> (the_unity_wrt F) holds ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 ) let T1, T2 be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative & F is having_an_inverseOp & F is having_a_unity & F .: (T1,T2) = i |-> (the_unity_wrt F) holds ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 ) let F be BinOp of D; ::_thesis: ( 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 ) ) assume A1: ( F is associative & F is having_an_inverseOp & F is having_a_unity & F .: (T1,T2) = i |-> (the_unity_wrt F) ) ; ::_thesis: ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 ) percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 ) then ( T1 = <*> D & T2 = <*> D ) ; hence ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 ) ; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 ) then reconsider C = Seg i as non empty set ; ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4; hence ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 ) by A1, Th72; ::_thesis: verum end; end; end; theorem Th75: :: FINSEQOP:75 for D, C being non empty set for e being Element of D for f being Function of C,D for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds G [;] (e,f) = C --> e proof let D, C be non empty set ; ::_thesis: for e being Element of D for f being Function of C,D for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds G [;] (e,f) = C --> e let e be Element of D; ::_thesis: for f being Function of C,D for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds G [;] (e,f) = C --> e let f be Function of C,D; ::_thesis: for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds G [;] (e,f) = C --> e let F, G be BinOp of D; ::_thesis: ( 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 ) 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 ) ; ::_thesis: G [;] (e,f) = C --> e now__::_thesis:_for_c_being_Element_of_C_holds_(G_[;]_(e,f))_._c_=_g_._c let c be Element of C; ::_thesis: (G [;] (e,f)) . c = g . c thus (G [;] (e,f)) . c = G . (e,(f . c)) by FUNCOP_1:53 .= e by A1, Th66 .= g . c by FUNCOP_1:7 ; ::_thesis: verum end; hence G [;] (e,f) = C --> e by FUNCT_2:63; ::_thesis: verum end; theorem :: FINSEQOP:76 for D being non empty set for e being Element of D for i being Nat for T being Tuple of i,D for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds G [;] (e,T) = i |-> e proof let D be non empty set ; ::_thesis: for e being Element of D for i being Nat for T being Tuple of i,D for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds G [;] (e,T) = i |-> e let e be Element of D; ::_thesis: for i being Nat for T being Tuple of i,D for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds G [;] (e,T) = i |-> e let i be Nat; ::_thesis: for T being Tuple of i,D for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds G [;] (e,T) = i |-> e let T be Tuple of i,D; ::_thesis: for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds G [;] (e,T) = i |-> e let F, G be BinOp of D; ::_thesis: ( 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 ) 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 ) ; ::_thesis: G [;] (e,T) = i |-> e percases ( i = 0 or i <> 0 ) ; supposeA2: i = 0 ; ::_thesis: G [;] (e,T) = i |-> e then G [;] (e,T) = <*> D by Lm2; hence G [;] (e,T) = i |-> e by A2; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: G [;] (e,T) = i |-> e then reconsider C = Seg i as non empty set ; T is Function of C,D by Lm4; hence G [;] (e,T) = i |-> e by A1, Th75; ::_thesis: verum end; end; end; definition let F, f, g be Function; funcF * (f,g) -> Function equals :: FINSEQOP:def 4 F * [:f,g:]; correctness coherence F * [:f,g:] is Function; ; end; :: deftheorem defines * FINSEQOP:def_4_:_ for F, f, g being Function holds F * (f,g) = F * [:f,g:]; theorem Th77: :: FINSEQOP:77 for x, y being set 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 x, y be set ; ::_thesis: 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)) let F, f, g be Function; ::_thesis: ( [x,y] in dom (F * (f,g)) implies (F * (f,g)) . (x,y) = F . ((f . x),(g . y)) ) assume A1: [x,y] in dom (F * (f,g)) ; ::_thesis: (F * (f,g)) . (x,y) = F . ((f . x),(g . y)) [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 (F * (f,g)) . (x,y) = F . ((f . x),(g . y)) by A1, FUNCT_1:12; ::_thesis: verum end; theorem :: FINSEQOP:78 for x, y being set 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)) by Th77; theorem Th79: :: FINSEQOP:79 for D, D9, E, C, C9 being non empty set for F being Function of [:D,D9:],E for f being Function of C,D for g being Function of C9,D9 holds F * (f,g) is Function of [:C,C9:],E proof let D, D9, E, C, C9 be non empty set ; ::_thesis: for F being Function of [:D,D9:],E for f being Function of C,D for g being Function of C9,D9 holds F * (f,g) is Function of [:C,C9:],E let F be Function of [:D,D9:],E; ::_thesis: for f being Function of C,D for g being Function of C9,D9 holds F * (f,g) is Function of [:C,C9:],E let f be Function of C,D; ::_thesis: for g being Function of C9,D9 holds F * (f,g) is Function of [:C,C9:],E let g be Function of C9,D9; ::_thesis: F * (f,g) is Function of [:C,C9:],E F * (f,g) = F * [:f,g:] ; hence F * (f,g) is Function of [:C,C9:],E ; ::_thesis: verum end; theorem :: FINSEQOP:80 for D being non empty set for F being BinOp of D for u, u9 being Function of D,D holds F * (u,u9) is BinOp of D by Th79; definition let D be non empty set ; let F be BinOp of D; let f, f9 be Function of D,D; :: original: * redefine funcF * (f,f9) -> BinOp of D; coherence F * (f,f9) is BinOp of D by Th79; end; theorem Th81: :: FINSEQOP:81 for D, D9, E, C, C9 being non empty set for c being Element of C for c9 being Element of C9 for F being Function of [:D,D9:],E for f being Function of C,D for g being Function of C9,D9 holds (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9)) proof let D, D9, E, C, C9 be non empty set ; ::_thesis: for c being Element of C for c9 being Element of C9 for F being Function of [:D,D9:],E for f being Function of C,D for g being Function of C9,D9 holds (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9)) let c be Element of C; ::_thesis: for c9 being Element of C9 for F being Function of [:D,D9:],E for f being Function of C,D for g being Function of C9,D9 holds (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9)) let c9 be Element of C9; ::_thesis: for F being Function of [:D,D9:],E for f being Function of C,D for g being Function of C9,D9 holds (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9)) let F be Function of [:D,D9:],E; ::_thesis: for f being Function of C,D for g being Function of C9,D9 holds (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9)) let f be Function of C,D; ::_thesis: for g being Function of C9,D9 holds (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9)) let g be Function of C9,D9; ::_thesis: (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9)) set H = F * (f,g); F * (f,g) is Function of [:C,C9:],E by Th79; then dom (F * (f,g)) = [:C,C9:] by FUNCT_2:def_1; then [c,c9] in dom (F * (f,g)) by ZFMISC_1:def_2; hence (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9)) by Th77; ::_thesis: verum end; theorem Th82: :: FINSEQOP:82 for D being non empty set for d1, d2 being Element of D for F being BinOp of D 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 D be non empty set ; ::_thesis: for d1, d2 being Element of D for F being BinOp of D 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) ) let d1, d2 be Element of D; ::_thesis: for F being BinOp of D 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) ) let F be BinOp of D; ::_thesis: 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) ) let u be Function of D,D; ::_thesis: ( (F * ((id D),u)) . (d1,d2) = F . (d1,(u . d2)) & (F * (u,(id D))) . (d1,d2) = F . ((u . d1),d2) ) ( (id D) . d1 = d1 & (id D) . d2 = d2 ) by FUNCT_1:18; hence ( (F * ((id D),u)) . (d1,d2) = F . (d1,(u . d2)) & (F * (u,(id D))) . (d1,d2) = F . ((u . d1),d2) ) by Th81; ::_thesis: verum end; theorem Th83: :: FINSEQOP:83 for C, D being non empty set for f, f9 being Function of C,D for F being BinOp of D for u being UnOp of D holds (F * ((id D),u)) .: (f,f9) = F .: (f,(u * f9)) proof let C, D be non empty set ; ::_thesis: for f, f9 being Function of C,D for F being BinOp of D for u being UnOp of D holds (F * ((id D),u)) .: (f,f9) = F .: (f,(u * f9)) let f, f9 be Function of C,D; ::_thesis: for F being BinOp of D for u being UnOp of D holds (F * ((id D),u)) .: (f,f9) = F .: (f,(u * f9)) let F be BinOp of D; ::_thesis: for u being UnOp of D holds (F * ((id D),u)) .: (f,f9) = F .: (f,(u * f9)) let u be UnOp of D; ::_thesis: (F * ((id D),u)) .: (f,f9) = F .: (f,(u * f9)) now__::_thesis:_for_c_being_Element_of_C_holds_((F_*_((id_D),u))_.:_(f,f9))_._c_=_(F_.:_(f,(u_*_f9)))_._c let c be Element of C; ::_thesis: ((F * ((id D),u)) .: (f,f9)) . c = (F .: (f,(u * f9))) . 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 Th82 .= F . ((f . c),((u * f9) . c)) by FUNCT_2:15 .= (F .: (f,(u * f9))) . c by FUNCOP_1:37 ; ::_thesis: verum end; hence (F * ((id D),u)) .: (f,f9) = F .: (f,(u * f9)) by FUNCT_2:63; ::_thesis: verum end; theorem :: FINSEQOP:84 for D being non empty set for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D for u being UnOp of D holds (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) proof let D be non empty set ; ::_thesis: for i being Nat for T1, T2 being Tuple of i,D for F being BinOp of D for u being UnOp of D holds (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) let i be Nat; ::_thesis: for T1, T2 being Tuple of i,D for F being BinOp of D for u being UnOp of D holds (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) let T1, T2 be Tuple of i,D; ::_thesis: for F being BinOp of D for u being UnOp of D holds (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) let F be BinOp of D; ::_thesis: for u being UnOp of D holds (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) let u be UnOp of D; ::_thesis: (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) now__::_thesis:_(F_*_((id_D),u))_.:_(T1,T2)_=_F_.:_(T1,(u_*_T2)) percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) then ( (F * ((id D),u)) .: (T1,T2) = <*> D & u * T2 = <*> D ) by Lm1; hence (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) by FINSEQ_2:73; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) then reconsider C = Seg i as non empty set ; ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4; hence (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) by Th83; ::_thesis: verum end; end; end; hence (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) ; ::_thesis: verum end; theorem :: FINSEQOP:85 for D being non empty set for d1, d2 being Element of D for F being BinOp of D for u being UnOp of D st F is associative & F is having_a_unity & F is commutative & F is having_an_inverseOp & u = the_inverseOp_wrt F holds ( 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 let D be non empty set ; ::_thesis: for d1, d2 being Element of D for F being BinOp of D for u being UnOp of D st F is associative & F is having_a_unity & F is commutative & F is having_an_inverseOp & u = the_inverseOp_wrt F holds ( 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)) ) let d1, d2 be Element of D; ::_thesis: for F being BinOp of D for u being UnOp of D st F is associative & F is having_a_unity & F is commutative & F is having_an_inverseOp & u = the_inverseOp_wrt F holds ( 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)) ) let F be BinOp of D; ::_thesis: for u being UnOp of D st F is associative & F is having_a_unity & F is commutative & F is having_an_inverseOp & u = the_inverseOp_wrt F holds ( 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)) ) let u be UnOp of D; ::_thesis: ( 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)) ) ) 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 ) ; ::_thesis: ( 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)) ) 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 Th82 .= F . ((u . d1),(u . (u . d2))) by A4, BINOP_1:def_12 .= F . ((u . d1),d2) by A1, A3, Th62 .= (F * (u,(id D))) . (d1,d2) by Th82 ; ::_thesis: (F * ((id D),u)) . (d1,d2) = u . ((F * (u,(id D))) . (d1,d2)) hence (F * ((id D),u)) . (d1,d2) = u . ((F * (u,(id D))) . (d1,d2)) by A1, A3, Th62; ::_thesis: verum end; theorem :: FINSEQOP:86 for D being non empty set for d being Element of D for F being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp holds (F * ((id D),(the_inverseOp_wrt F))) . (d,d) = the_unity_wrt F proof let D be non empty set ; ::_thesis: for d being Element of D for F being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp holds (F * ((id D),(the_inverseOp_wrt F))) . (d,d) = the_unity_wrt F let d be Element of D; ::_thesis: for F being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp holds (F * ((id D),(the_inverseOp_wrt F))) . (d,d) = the_unity_wrt F let F be BinOp of D; ::_thesis: ( 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 ) assume A1: ( F is associative & F is having_a_unity & F is having_an_inverseOp ) ; ::_thesis: (F * ((id D),(the_inverseOp_wrt F))) . (d,d) = the_unity_wrt F set u = the_inverseOp_wrt F; thus (F * ((id D),(the_inverseOp_wrt F))) . (d,d) = F . (d,((the_inverseOp_wrt F) . d)) by Th82 .= the_unity_wrt F by A1, Th59 ; ::_thesis: verum end; theorem :: FINSEQOP:87 for D being non empty set for d being Element of D for F being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp holds (F * ((id D),(the_inverseOp_wrt F))) . (d,(the_unity_wrt F)) = d proof let D be non empty set ; ::_thesis: for d being Element of D for F being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp holds (F * ((id D),(the_inverseOp_wrt F))) . (d,(the_unity_wrt F)) = d let d be Element of D; ::_thesis: for F being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp holds (F * ((id D),(the_inverseOp_wrt F))) . (d,(the_unity_wrt F)) = d let F be BinOp of D; ::_thesis: ( 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 ) assume that A1: F is associative and A2: F is having_a_unity and A3: F is having_an_inverseOp ; ::_thesis: (F * ((id D),(the_inverseOp_wrt F))) . (d,(the_unity_wrt F)) = d set u = the_inverseOp_wrt F; set e = the_unity_wrt F; thus (F * ((id D),(the_inverseOp_wrt F))) . (d,(the_unity_wrt F)) = F . (d,((the_inverseOp_wrt F) . (the_unity_wrt F))) by Th82 .= F . (d,(the_unity_wrt F)) by A1, A2, A3, Th61 .= d by A2, SETWISEO:15 ; ::_thesis: verum end; theorem :: FINSEQOP:88 for D being non empty set for d being Element of D for F being BinOp of D for u being UnOp of D st F is having_a_unity holds (F * ((id D),u)) . ((the_unity_wrt F),d) = u . d proof let D be non empty set ; ::_thesis: for d being Element of D for F being BinOp of D for u being UnOp of D st F is having_a_unity holds (F * ((id D),u)) . ((the_unity_wrt F),d) = u . d let d be Element of D; ::_thesis: for F being BinOp of D for u being UnOp of D st F is having_a_unity holds (F * ((id D),u)) . ((the_unity_wrt F),d) = u . d let F be BinOp of D; ::_thesis: for u being UnOp of D st F is having_a_unity holds (F * ((id D),u)) . ((the_unity_wrt F),d) = u . d let u be UnOp of D; ::_thesis: ( F is having_a_unity implies (F * ((id D),u)) . ((the_unity_wrt F),d) = u . d ) assume A1: F is having_a_unity ; ::_thesis: (F * ((id D),u)) . ((the_unity_wrt F),d) = u . d set e = the_unity_wrt F; thus (F * ((id D),u)) . ((the_unity_wrt F),d) = F . ((the_unity_wrt F),(u . d)) by Th82 .= u . d by A1, SETWISEO:15 ; ::_thesis: verum end; theorem :: FINSEQOP:89 for D being non empty set for F, G being BinOp of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G = F * ((id D),(the_inverseOp_wrt F)) holds for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) proof let D be non empty set ; ::_thesis: for F, G being BinOp of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G = F * ((id D),(the_inverseOp_wrt F)) holds for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) let F, G be BinOp of D; ::_thesis: ( 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 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) 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)) ; ::_thesis: for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) set u = the_inverseOp_wrt F; A5: the_inverseOp_wrt F is_distributive_wrt F by A1, A2, A3, Th63; let d1, d2, d3, d4 be Element of D; ::_thesis: F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) thus F . ((G . (d1,d2)),(G . (d3,d4))) = F . ((F . (d1,((the_inverseOp_wrt F) . d2))),(G . (d3,d4))) by A4, Th82 .= F . ((F . (d1,((the_inverseOp_wrt F) . d2))),(F . (d3,((the_inverseOp_wrt F) . d4)))) by A4, Th82 .= F . (d1,(F . (((the_inverseOp_wrt F) . d2),(F . (d3,((the_inverseOp_wrt F) . d4)))))) by A2, BINOP_1:def_3 .= F . (d1,(F . ((F . (((the_inverseOp_wrt F) . d2),d3)),((the_inverseOp_wrt F) . d4)))) by A2, BINOP_1:def_3 .= F . (d1,(F . ((F . (d3,((the_inverseOp_wrt F) . d2))),((the_inverseOp_wrt F) . d4)))) by A1, BINOP_1:def_2 .= F . (d1,(F . (d3,(F . (((the_inverseOp_wrt F) . d2),((the_inverseOp_wrt F) . d4)))))) by A2, BINOP_1:def_3 .= F . ((F . (d1,d3)),(F . (((the_inverseOp_wrt F) . d2),((the_inverseOp_wrt F) . d4)))) by A2, BINOP_1:def_3 .= F . ((F . (d1,d3)),((the_inverseOp_wrt F) . (F . (d2,d4)))) by A5, BINOP_1:def_12 .= G . ((F . (d1,d3)),(F . (d2,d4))) by A4, Th82 ; ::_thesis: verum end;