:: Binary Operations Applied to Finite Sequences
:: by Czes{\l}aw Byli\'nski
::
:: Received May 4, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

:: Auxiliary theorems
theorem Th1: :: FINSEQOP:1
for f being Function holds
( <:{},f:> = {} &amp; <:f,{}:> = {} )
proofend;

theorem :: FINSEQOP:2
for f being Function holds
( [:{},f:] = {} &amp; [:f,{}:] = {} )
proofend;

theorem Th3: :: FINSEQOP:3
for F, f being Function holds
( F .: ({},f) = {} &amp; F .: (f,{}) = {} )
proofend;

theorem :: FINSEQOP:4
for x being set
for F being Function holds F [:] ({},x) = {}
proofend;

theorem :: FINSEQOP:5
for x being set
for F being Function holds F [;] (x,{}) = {}
proofend;

theorem Th6: :: FINSEQOP:6
for X, x1, x2 being set holds <:(X --> x1),(X --> x2):> = X --> [x1,x2]
proofend;

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))
proofend;

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)*>
proofend;

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)
proofend;

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
proofend;

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
proofend;

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
proofend;

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))*>
proofend;

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))
proofend;

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))*>
proofend;

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))
proofend;

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))*>
proofend;

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))
proofend;

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)
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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
proofend;

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
proofend;

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)
proofend;

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))
proofend;

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)
proofend;

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))
proofend;

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)))
proofend;

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)))
proofend;

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)))
proofend;

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)))
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)))
proofend;

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)))
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

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 &amp; F .: (f,(C --> (the_unity_wrt F))) = f )
proofend;

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
proofend;

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
proofend;

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)))
proofend;

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)))
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

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 &amp; u = G [;] (d,(id D)) holds
u is_distributive_wrt F
proofend;

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 &amp; u = G [:] ((id D),d) holds
u is_distributive_wrt F
proofend;

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 &amp; F .: (T,(i |-> (the_unity_wrt F))) = T )
proofend;

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
proofend;

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
proofend;

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 &amp; 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 &amp; 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 &amp; b2 is_an_inverseOp_wrt F holds
b1 = b2
proofend;
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 &amp; F is associative &amp; 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 &amp; F is associative &amp; F is having_an_inverseOp holds
( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F &amp; F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F )
proofend;

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 &amp; F is associative &amp; F is having_an_inverseOp &amp; F . (d1,d2) = the_unity_wrt F holds
( d1 = (the_inverseOp_wrt F) . d2 &amp; (the_inverseOp_wrt F) . d1 = d2 )
proofend;

theorem Th61: :: FINSEQOP:61
for D being non empty set
for F being BinOp of D st F is having_a_unity &amp; F is associative &amp; F is having_an_inverseOp holds
(the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F
proofend;

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 &amp; F is associative &amp; F is having_an_inverseOp holds
(the_inverseOp_wrt F) . ((the_inverseOp_wrt F) . d) = d
proofend;

theorem Th63: :: FINSEQOP:63
for D being non empty set
for F being BinOp of D st F is having_a_unity &amp; F is associative &amp; F is commutative &amp; F is having_an_inverseOp holds
the_inverseOp_wrt F is_distributive_wrt F
proofend;

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 &amp; F is associative &amp; F is having_an_inverseOp &amp; ( F . (d,d1) = F . (d,d2) or F . (d1,d) = F . (d2,d) ) holds
d1 = d2
proofend;

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 &amp; F is associative &amp; F is having_an_inverseOp &amp; ( F . (d1,d2) = d2 or F . (d2,d1) = d2 ) holds
d1 = the_unity_wrt F
proofend;

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 &amp; F is having_a_unity &amp; F is having_an_inverseOp &amp; G is_distributive_wrt F &amp; e = the_unity_wrt F holds
for d being Element of D holds
( G . (e,d) = e &amp; G . (d,e) = e )
proofend;

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 &amp; F is associative &amp; F is having_an_inverseOp &amp; u = the_inverseOp_wrt F &amp; G is_distributive_wrt F holds
( u . (G . (d1,d2)) = G . ((u . d1),d2) &amp; u . (G . (d1,d2)) = G . (d1,(u . d2)) )
proofend;

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 &amp; F is associative &amp; F is having_an_inverseOp &amp; u = the_inverseOp_wrt F &amp; G is_distributive_wrt F &amp; G is having_a_unity holds
G [;] ((u . (the_unity_wrt G)),(id D)) = u
proofend;

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 &amp; F is having_a_unity &amp; F is having_an_inverseOp &amp; G is_distributive_wrt F holds
(G [;] (d,(id D))) . (the_unity_wrt F) = the_unity_wrt F
proofend;

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 &amp; F is having_a_unity &amp; F is having_an_inverseOp &amp; G is_distributive_wrt F holds
(G [:] ((id D),d)) . (the_unity_wrt F) = the_unity_wrt F
proofend;

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 &amp; F is associative &amp; F is having_an_inverseOp holds
( F .: (f,((the_inverseOp_wrt F) * f)) = C --> (the_unity_wrt F) &amp; F .: (((the_inverseOp_wrt F) * f),f) = C --> (the_unity_wrt F) )
proofend;

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 &amp; F is having_an_inverseOp &amp; F is having_a_unity &amp; F .: (f,f9) = C --> (the_unity_wrt F) holds
( f = (the_inverseOp_wrt F) * f9 &amp; (the_inverseOp_wrt F) * f = f9 )
proofend;

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 &amp; F is associative &amp; F is having_an_inverseOp holds
( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) &amp; F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) )
proofend;

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 &amp; F is having_an_inverseOp &amp; F is having_a_unity &amp; F .: (T1,T2) = i |-> (the_unity_wrt F) holds
( T1 = (the_inverseOp_wrt F) * T2 &amp; (the_inverseOp_wrt F) * T1 = T2 )
proofend;

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 &amp; F is having_a_unity &amp; e = the_unity_wrt F &amp; F is having_an_inverseOp &amp; G is_distributive_wrt F holds
G [;] (e,f) = C --> e
proofend;

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 &amp; F is having_a_unity &amp; e = the_unity_wrt F &amp; F is having_an_inverseOp &amp; G is_distributive_wrt F holds
G [;] (e,T) = i |-> e
proofend;

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))
proofend;

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
proofend;

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))
proofend;

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)) &amp; (F * (u,(id D))) . (d1,d2) = F . ((u . d1),d2) )
proofend;

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))
proofend;

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))
proofend;

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 &amp; F is having_a_unity &amp; F is commutative &amp; F is having_an_inverseOp &amp; u = the_inverseOp_wrt F holds
( u . ((F * ((id D),u)) . (d1,d2)) = (F * (u,(id D))) . (d1,d2) &amp; (F * ((id D),u)) . (d1,d2) = u . ((F * (u,(id D))) . (d1,d2)) )
proofend;

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 &amp; F is having_a_unity &amp; F is having_an_inverseOp holds
(F * ((id D),(the_inverseOp_wrt F))) . (d,d) = the_unity_wrt F
proofend;

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 &amp; F is having_a_unity &amp; F is having_an_inverseOp holds
(F * ((id D),(the_inverseOp_wrt F))) . (d,(the_unity_wrt F)) = d
proofend;

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
proofend;

theorem :: FINSEQOP:89
for D being non empty set
for F, G being BinOp of D st F is commutative &amp; F is associative &amp; F is having_a_unity &amp; F is having_an_inverseOp &amp; 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)))
proofend;