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

begin

theorem Th1: :: FINSEQOP:1

for f being Function holds
( <:{},f:> = {} & <:f,{}:> = {} )

proof end;

theorem :: FINSEQOP:2

for f being Function holds
( [:{},f:] = {} & [:f,{}:] = {} )

proof end;

theorem :: FINSEQOP:3

canceled;

theorem Th4: :: FINSEQOP:4

for F, f being Function holds
( F .: ({},f) = {} & F .: (f,{}) = {} )

proof end;

theorem :: FINSEQOP:5

for x being set
for F being Function holds F [:] ({},x) = {}

proof end;

theorem :: FINSEQOP:6

for x being set
for F being Function holds F [;] (x,{}) = {}

proof end;

theorem Th7: :: FINSEQOP:7

for X, x1, x2 being set holds <:(X --> x1),(X --> x2):> = X --> [x1,x2]

proof end;

theorem Th8: :: FINSEQOP:8

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 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 func F .: (p,p9) -> FinSequence of E;
coherence
F .: (p,p9) is FinSequence of E by FINSEQ_2:84;

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 func F [:] (p,d9) -> FinSequence of E;
coherence
F [:] (p,d9) is FinSequence of E by FINSEQ_2:97;

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 func F [;] (d,p9) -> FinSequence of E;
coherence
F [;] (d,p9) is FinSequence of E by FINSEQ_2:91;

end;

definition

let D be non empty set ;
let i be Nat;
let d be Element of D;
:: original: |->
redefine func i |-> d -> Element of i -tuples_on D;
coherence
i |-> d is Element of i -tuples_on D by FINSEQ_2:132;

end;

definition

let D, E be set ;
let p be FinSequence of D;
let h be Function of D,E;
:: original: *
redefine func h * p -> FinSequence of E;
coherence
p * h is FinSequence of E by FINSEQ_2:36;

end;

theorem Th9: :: FINSEQOP:9

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

theorem :: FINSEQOP:10

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

theorem Th11: :: FINSEQOP:11

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

theorem :: FINSEQOP:12

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

theorem Th13: :: FINSEQOP:13

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

theorem :: FINSEQOP:14

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

theorem Th15: :: FINSEQOP:15

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

theorem :: FINSEQOP:16

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

theorem :: FINSEQOP:17

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

theorem Th18: :: 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 .: ((i |-> d),(i |-> d9)) = i |-> (F . (d,d9))

proof 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 [;] (d,(i |-> d9)) = i |-> (F . (d,d9))

proof end;

theorem :: FINSEQOP:20

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

theorem :: FINSEQOP:21

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

theorem :: FINSEQOP:22

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

theorem :: FINSEQOP:23

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

theorem :: FINSEQOP:24

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 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 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 [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9)

proof end;

theorem Th26: :: FINSEQOP:26

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 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 [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2)

proof end;

theorem :: FINSEQOP:28

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

theorem :: FINSEQOP:29

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

theorem :: FINSEQOP:30

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

theorem :: FINSEQOP:31

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 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 [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T)))

proof end;

theorem :: FINSEQOP:33

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

theorem :: FINSEQOP:34

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

theorem :: FINSEQOP:35

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 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 [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f)))

proof end;

theorem Th37: :: FINSEQOP:37

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

theorem Th38: :: FINSEQOP:38

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 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 [;] (d,f)) = H [;] ((h . d),(h * f))

proof end;

theorem Th40: :: FINSEQOP:40

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

theorem :: FINSEQOP:41

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 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 [;] (d,f)) = F [;] ((u . d),(u * f))

proof end;

theorem :: FINSEQOP:43

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

theorem Th44: :: FINSEQOP:44

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 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 [;] ((the_unity_wrt F),f) = f

proof end;

theorem Th46: :: FINSEQOP:46

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 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 [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T)))

proof end;

theorem :: FINSEQOP:48

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

theorem Th49: :: FINSEQOP:49

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 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 [;] (d,T)) = H [;] ((h . d),(h * T))

proof end;

theorem Th51: :: FINSEQOP:51

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

theorem :: FINSEQOP:52

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 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 [;] (d,T)) = F [;] ((u . d),(u * T))

proof end;

theorem :: FINSEQOP:54

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

proof end;

theorem :: FINSEQOP:56

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

proof 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 [;] ((the_unity_wrt F),T) = T

proof end;

theorem :: FINSEQOP:59

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

definition

let D be non empty set ;
let u be UnOp of D;
let F be BinOp of D;
pred u 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;
attr F 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 b₁ being UnOp of D st b₁ is_an_inverseOp_wrt F by A3, Def2;
uniqueness
for b₁, b₂ being UnOp of D st b₁ is_an_inverseOp_wrt F & b₂ is_an_inverseOp_wrt F holds
b₁ = b₂

proof 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 b₃ being UnOp of D holds
( b₃ = the_inverseOp_wrt F iff b₃ is_an_inverseOp_wrt F );

theorem :: FINSEQOP:60

canceled;

theorem :: FINSEQOP:61

canceled;

theorem :: FINSEQOP:62

canceled;

theorem Th63: :: FINSEQOP:63

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

theorem Th64: :: FINSEQOP:64

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

theorem Th65: :: FINSEQOP:65

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

theorem Th66: :: FINSEQOP:66

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

theorem Th67: :: FINSEQOP:67

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

theorem Th68: :: FINSEQOP:68

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

theorem Th69: :: FINSEQOP:69

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

theorem Th70: :: FINSEQOP:70

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

theorem Th71: :: FINSEQOP:71

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

theorem :: FINSEQOP:72

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

theorem :: FINSEQOP:73

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

theorem :: FINSEQOP:74

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

theorem Th75: :: FINSEQOP:75

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

theorem Th76: :: FINSEQOP:76

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

theorem :: FINSEQOP:77

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

theorem :: FINSEQOP:78

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

theorem Th79: :: FINSEQOP:79

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

theorem :: FINSEQOP:80

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

definition

let F, f, g be Function;
func F * (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 :: FINSEQOP:81

canceled;

theorem Th82: :: FINSEQOP:82

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

theorem :: FINSEQOP:83

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

theorem Th84: :: FINSEQOP:84

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

theorem :: FINSEQOP:85

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

definition

let D be non empty set ;
let F be BinOp of D;
let f, f9 be Function of D,D;
:: original: *
redefine func F * (f,f9) -> BinOp of D;
coherence
F * (f,f9) is BinOp of D by Th84;

end;

theorem Th86: :: FINSEQOP:86

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

theorem Th87: :: FINSEQOP:87

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

theorem Th88: :: FINSEQOP:88

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

theorem :: FINSEQOP:89

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

theorem :: FINSEQOP:90

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

theorem :: FINSEQOP:91

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

theorem :: FINSEQOP:92

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

theorem :: FINSEQOP:93

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

theorem :: FINSEQOP:94

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