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

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, D', E be non empty set ;
let F be Function of [:D,D':],E;
let p be FinSequence of D;
let p' be FinSequence of D';
:: original: .:
redefine func F .: p,p' -> FinSequence of E;
coherence
F .: p,p' is FinSequence of E by FINSEQ_2:84;

end;

definition

let D, D', E be non empty set ;
let F be Function of [:D,D':],E;
let p be FinSequence of D;
let d' be Element of D';
:: original: [:]
redefine func F [:] p,d' -> FinSequence of E;
coherence
F [:] p,d' is FinSequence of E by FINSEQ_2:97;

end;

definition

let D, D', E be non empty set ;
let F be Function of [:D,D':],E;
let d be Element of D;
let p' be FinSequence of D';
:: original: [;]
redefine func F [;] d,p' -> FinSequence of E;
coherence
F [;] d,p' 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 C, D being non empty set
for f being Function of C,D
for T being Element of 0 -tuples_on C holds f * T = <*> D

proof end;

Lm2: for D', D, E being non empty set
for i being Nat
for F being Function of [:D,D':],E
for T' being Element of i -tuples_on D'
for T being Element of 0 -tuples_on D holds F .: T,T' = <*> E

proof end;

Lm3: for D, D', E being non empty set
for d being Element of D
for F being Function of [:D,D':],E
for T' being Element of 0 -tuples_on D' holds F [;] d,T' = <*> E

proof end;

Lm4: for D', D, E being non empty set
for d' being Element of D'
for F being Function of [:D,D':],E
for T being Element of 0 -tuples_on D holds F [:] T,d' = <*> E

proof end;

theorem Th11: :: FINSEQOP:11

for E, D, D' being non empty set
for d being Element of D
for d' being Element of D'
for i being Nat
for F being Function of [:D,D':],E
for T being Element of i -tuples_on D
for T' being Element of i -tuples_on D' holds F .: (T ^ <*d*>),(T' ^ <*d'*>) = (F .: T,T') ^ <*(F . d,d')*>

proof end;

theorem :: FINSEQOP:12

for E, D, D' being non empty set
for i, j being Nat
for F being Function of [:D,D':],E
for T being Element of i -tuples_on D
for T' being Element of i -tuples_on D'
for S being Element of j -tuples_on D
for S' being Element of j -tuples_on D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')

proof end;

theorem Th13: :: FINSEQOP:13

for D, E, D' being non empty set
for d being Element of D
for d' being Element of D'
for F being Function of [:D,D':],E
for p' being FinSequence of D' holds F [;] d,(p' ^ <*d'*>) = (F [;] d,p') ^ <*(F . d,d')*>

proof end;

theorem :: FINSEQOP:14

for D, E, D' being non empty set
for d being Element of D
for F being Function of [:D,D':],E
for p', q' being FinSequence of D' holds F [;] d,(p' ^ q') = (F [;] d,p') ^ (F [;] d,q')

proof end;

theorem Th15: :: FINSEQOP:15

for D', E, D being non empty set
for d being Element of D
for d' being Element of D'
for F being Function of [:D,D':],E
for p being FinSequence of D holds F [:] (p ^ <*d*>),d' = (F [:] p,d') ^ <*(F . d,d')*>

proof end;

theorem :: FINSEQOP:16

for D', E, D being non empty set
for d' being Element of D'
for F being Function of [:D,D':],E
for p, q being FinSequence of D holds F [:] (p ^ q),d' = (F [:] p,d') ^ (F [:] q,d')

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, D', E being non empty set
for d being Element of D
for d' being Element of D'
for i being Nat
for F being Function of [:D,D':],E holds F .: (i |-> d),(i |-> d') = i |-> (F . d,d')

proof end;

theorem :: FINSEQOP:19

for D, D', E being non empty set
for d being Element of D
for d' being Element of D'
for i being Nat
for F being Function of [:D,D':],E holds F [;] d,(i |-> d') = i |-> (F . d,d')

proof end;

theorem :: FINSEQOP:20

for D, D', E being non empty set
for d being Element of D
for d' being Element of D'
for i being Nat
for F being Function of [:D,D':],E holds F [:] (i |-> d),d' = i |-> (F . d,d')

proof end;

theorem :: FINSEQOP:21

for D, E, D' being non empty set
for d being Element of D
for i being Nat
for F being Function of [:D,D':],E
for T' being Element of i -tuples_on D' holds F .: (i |-> d),T' = F [;] d,T'

proof end;

theorem :: FINSEQOP:22

for D', E, D being non empty set
for d being Element of D
for i being Nat
for F being Function of [:D,D':],E
for T being Element of i -tuples_on D holds F .: T,(i |-> d) = F [:] T,d

proof end;

theorem :: FINSEQOP:23

for D, E, D' being non empty set
for d being Element of D
for i being Nat
for F being Function of [:D,D':],E
for T' being Element of i -tuples_on D' holds F [;] d,T' = (F [;] d,(id D')) * T'

proof end;

theorem :: FINSEQOP:24

for D', E, D being non empty set
for d being Element of D
for i being Nat
for F being Function of [:D,D':],E
for T being Element of i -tuples_on D holds F [:] T,d = (F [:] (id D),d) * T

proof end;

Lm5: for D being non empty set
for i being Nat
for T being Element of i -tuples_on 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, f' being Function of C,D
for F being BinOp of D st F is associative holds
(F [;] d,(id D)) * (F .: f,f') = F .: ((F [;] d,(id D)) * f),f'

proof end;

theorem Th26: :: FINSEQOP:26

for C, D being non empty set
for d being Element of D
for f, f' being Function of C,D
for F being BinOp of D st F is associative holds
(F [:] (id D),d) * (F .: f,f') = F .: f,((F [:] (id D),d) * f')

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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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, 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,f') = H .: (h * f),(h * f')

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, 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,f') = F .: (u * f),(u * f')

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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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, f' 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,f' = C --> (the_unity_wrt F) holds
( f = (the_inverseOp_wrt F) * f' & (the_inverseOp_wrt F) * f = f' )

proof end;

theorem :: FINSEQOP:77

for D being non empty set
for i being Nat
for T being Element of i -tuples_on 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 Element of i -tuples_on 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 Element of i -tuples_on 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, D', E, C, C' being non empty set
for F being Function of [:D,D':],E
for f being Function of C,D
for g being Function of C',D' holds F * f,g is Function of [:C,C':],E

proof end;

theorem :: FINSEQOP:85

for D being non empty set
for F being BinOp of D
for u, u' being Function of D,D holds F * u,u' is BinOp of D by Th84;

definition

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

end;

theorem Th86: :: FINSEQOP:86

for D, D', E, C, C' being non empty set
for c being Element of C
for c' being Element of C'
for F being Function of [:D,D':],E
for f being Function of C,D
for g being Function of C',D' holds (F * f,g) . c,c' = F . (f . c),(g . c')

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, f' being Function of C,D
for F being BinOp of D
for u being UnOp of D holds (F * (id D),u) .: f,f' = F .: f,(u * f')

proof end;

theorem :: FINSEQOP:89

for D being non empty set
for i being Nat
for T1, T2 being Element of i -tuples_on 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 associative & F is having_a_unity & F is having_an_inverseOp & u = the_inverseOp_wrt F 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;