:: FINSEQOP semantic presentation

theorem Th1: :: FINSEQOP:1
for b1 being Function holds
( <:{} ,b1:> = {} & <:b1,{} :> = {} )
proof end;

theorem Th2: :: FINSEQOP:2
for b1 being Function holds
( [:{} ,b1:] = {} & [:b1,{} :] = {} )
proof end;

theorem Th3: :: FINSEQOP:3
canceled;

theorem Th4: :: FINSEQOP:4
for b1, b2 being Function holds
( b1 .: {} ,b2 = {} & b1 .: b2,{} = {} )
proof end;

theorem Th5: :: FINSEQOP:5
for b1 being set
for b2 being Function holds b2 [:] {} ,b1 = {}
proof end;

theorem Th6: :: FINSEQOP:6
for b1 being set
for b2 being Function holds b2 [;] b1,{} = {}
proof end;

theorem Th7: :: FINSEQOP:7
for b1, b2, b3 being set holds <:(b1 --> b2),(b1 --> b3):> = b1 --> [b2,b3]
proof end;

theorem Th8: :: FINSEQOP:8
for b1 being Function
for b2, b3, b4 being set st [b3,b4] in dom b1 holds
b1 .: (b2 --> b3),(b2 --> b4) = b2 --> (b1 . [b3,b4])
proof end;

definition
let c1, c2, c3 be non empty set ;
let c4 be Function of [:c1,c2:],c3;
let c5 be FinSequence of c1;
let c6 be FinSequence of c2;
redefine func .: as c4 .: c5,c6 -> FinSequence of a3;
coherence
c4 .: c5,c6 is FinSequence of c3 by FINSEQ_2:84;
end;

definition
let c1, c2, c3 be non empty set ;
let c4 be Function of [:c1,c2:],c3;
let c5 be FinSequence of c1;
let c6 be Element of c2;
redefine func [:] as c4 [:] c5,c6 -> FinSequence of a3;
coherence
c4 [:] c5,c6 is FinSequence of c3 by FINSEQ_2:97;
end;

definition
let c1, c2, c3 be non empty set ;
let c4 be Function of [:c1,c2:],c3;
let c5 be Element of c1;
let c6 be FinSequence of c2;
redefine func [;] as c4 [;] c5,c6 -> FinSequence of a3;
coherence
c4 [;] c5,c6 is FinSequence of c3 by FINSEQ_2:91;
end;

definition
let c1 be non empty set ;
let c2 be Nat;
let c3 be Element of c1;
redefine func |-> as c2 |-> c3 -> Element of a2 -tuples_on a1;
coherence
c2 |-> c3 is Element of c2 -tuples_on c1 by FINSEQ_2:132;
end;

definition
let c1, c2 be set ;
let c3 be FinSequence of c1;
let c4 be Function of c1,c2;
redefine func * as c4 * c3 -> FinSequence of a2;
coherence
c3 * c4 is FinSequence of c2 by FINSEQ_2:36;
end;

theorem Th9: :: FINSEQOP:9
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being FinSequence of b1
for b5 being Function of b1,b2 holds b5 * (b4 ^ <*b3*>) = (b5 * b4) ^ <*(b5 . b3)*>
proof end;

theorem Th10: :: FINSEQOP:10
for b1, b2 being non empty set
for b3, b4 being FinSequence of b1
for b5 being Function of b1,b2 holds b5 * (b3 ^ b4) = (b5 * b3) ^ (b5 * b4)
proof end;

Lemma6: for b1, b2 being non empty set
for b3 being Function of b1,b2
for b4 being Element of 0 -tuples_on b1 holds b3 * b4 = <*> b2
proof end;

Lemma7: for b1, b2, b3 being non empty set
for b4 being Nat
for b5 being Function of [:b2,b1:],b3
for b6 being Element of b4 -tuples_on b1
for b7 being Element of 0 -tuples_on b2 holds b5 .: b7,b6 = <*> b3
proof end;

Lemma8: for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being Function of [:b1,b2:],b3
for b6 being Element of 0 -tuples_on b2 holds b5 [;] b4,b6 = <*> b3
proof end;

Lemma9: for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being Function of [:b2,b1:],b3
for b6 being Element of 0 -tuples_on b2 holds b5 [:] b6,b4 = <*> b3
proof end;

theorem Th11: :: FINSEQOP:11
for b1, b2, b3 being non empty set
for b4 being Element of b2
for b5 being Element of b3
for b6 being Nat
for b7 being Function of [:b2,b3:],b1
for b8 being Element of b6 -tuples_on b2
for b9 being Element of b6 -tuples_on b3 holds b7 .: (b8 ^ <*b4*>),(b9 ^ <*b5*>) = (b7 .: b8,b9) ^ <*(b7 . b4,b5)*>
proof end;

theorem Th12: :: FINSEQOP:12
for b1, b2, b3 being non empty set
for b4, b5 being Nat
for b6 being Function of [:b2,b3:],b1
for b7 being Element of b4 -tuples_on b2
for b8 being Element of b4 -tuples_on b3
for b9 being Element of b5 -tuples_on b2
for b10 being Element of b5 -tuples_on b3 holds b6 .: (b7 ^ b9),(b8 ^ b10) = (b6 .: b7,b8) ^ (b6 .: b9,b10)
proof end;

theorem Th13: :: FINSEQOP:13
for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being Element of b3
for b6 being Function of [:b1,b3:],b2
for b7 being FinSequence of b3 holds b6 [;] b4,(b7 ^ <*b5*>) = (b6 [;] b4,b7) ^ <*(b6 . b4,b5)*>
proof end;

theorem Th14: :: FINSEQOP:14
for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being Function of [:b1,b3:],b2
for b6, b7 being FinSequence of b3 holds b5 [;] b4,(b6 ^ b7) = (b5 [;] b4,b6) ^ (b5 [;] b4,b7)
proof end;

theorem Th15: :: FINSEQOP:15
for b1, b2, b3 being non empty set
for b4 being Element of b3
for b5 being Element of b1
for b6 being Function of [:b3,b1:],b2
for b7 being FinSequence of b3 holds b6 [:] (b7 ^ <*b4*>),b5 = (b6 [:] b7,b5) ^ <*(b6 . b4,b5)*>
proof end;

theorem Th16: :: FINSEQOP:16
for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being Function of [:b3,b1:],b2
for b6, b7 being FinSequence of b3 holds b5 [:] (b6 ^ b7),b4 = (b5 [:] b6,b4) ^ (b5 [:] b7,b4)
proof end;

theorem Th17: :: FINSEQOP:17
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being Nat
for b5 being Function of b1,b2 holds b5 * (b4 |-> b3) = b4 |-> (b5 . b3)
proof end;

theorem Th18: :: FINSEQOP:18
for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being Element of b2
for b6 being Nat
for b7 being Function of [:b1,b2:],b3 holds b7 .: (b6 |-> b4),(b6 |-> b5) = b6 |-> (b7 . b4,b5)
proof end;

theorem Th19: :: FINSEQOP:19
for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being Element of b2
for b6 being Nat
for b7 being Function of [:b1,b2:],b3 holds b7 [;] b4,(b6 |-> b5) = b6 |-> (b7 . b4,b5)
proof end;

theorem Th20: :: FINSEQOP:20
for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being Element of b2
for b6 being Nat
for b7 being Function of [:b1,b2:],b3 holds b7 [:] (b6 |-> b4),b5 = b6 |-> (b7 . b4,b5)
proof end;

theorem Th21: :: FINSEQOP:21
for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being Nat
for b6 being Function of [:b1,b3:],b2
for b7 being Element of b5 -tuples_on b3 holds b6 .: (b5 |-> b4),b7 = b6 [;] b4,b7
proof end;

theorem Th22: :: FINSEQOP:22
for b1, b2, b3 being non empty set
for b4 being Element of b3
for b5 being Nat
for b6 being Function of [:b3,b1:],b2
for b7 being Element of b5 -tuples_on b3 holds b6 .: b7,(b5 |-> b4) = b6 [:] b7,b4
proof end;

theorem Th23: :: FINSEQOP:23
for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being Nat
for b6 being Function of [:b1,b3:],b2
for b7 being Element of b5 -tuples_on b3 holds b6 [;] b4,b7 = (b6 [;] b4,(id b3)) * b7
proof end;

theorem Th24: :: FINSEQOP:24
for b1, b2, b3 being non empty set
for b4 being Element of b3
for b5 being Nat
for b6 being Function of [:b3,b1:],b2
for b7 being Element of b5 -tuples_on b3 holds b6 [:] b7,b4 = (b6 [:] (id b3),b4) * b7
proof end;

Lemma14: for b1 being non empty set
for b2 being Nat
for b3 being Element of b2 -tuples_on b1 holds b3 is Function of Seg b2,b1
proof end;

theorem Th25: :: FINSEQOP:25
for b1, b2 being non empty set
for b3 being Element of b2
for b4, b5 being Function of b1,b2
for b6 being BinOp of b2 st b6 is associative holds
(b6 [;] b3,(id b2)) * (b6 .: b4,b5) = b6 .: ((b6 [;] b3,(id b2)) * b4),b5
proof end;

theorem Th26: :: FINSEQOP:26
for b1, b2 being non empty set
for b3 being Element of b2
for b4, b5 being Function of b1,b2
for b6 being BinOp of b2 st b6 is associative holds
(b6 [:] (id b2),b3) * (b6 .: b4,b5) = b6 .: b4,((b6 [:] (id b2),b3) * b5)
proof end;

theorem Th27: :: FINSEQOP:27
for b1 being non empty set
for b2 being Element of b1
for b3 being Nat
for b4, b5 being Element of b3 -tuples_on b1
for b6 being BinOp of b1 st b6 is associative holds
(b6 [;] b2,(id b1)) * (b6 .: b4,b5) = b6 .: ((b6 [;] b2,(id b1)) * b4),b5
proof end;

theorem Th28: :: FINSEQOP:28
for b1 being non empty set
for b2 being Element of b1
for b3 being Nat
for b4, b5 being Element of b3 -tuples_on b1
for b6 being BinOp of b1 st b6 is associative holds
(b6 [:] (id b1),b2) * (b6 .: b4,b5) = b6 .: b4,((b6 [:] (id b1),b2) * b5)
proof end;

theorem Th29: :: FINSEQOP:29
for b1 being non empty set
for b2 being Nat
for b3, b4, b5 being Element of b2 -tuples_on b1
for b6 being BinOp of b1 st b6 is associative holds
b6 .: (b6 .: b3,b4),b5 = b6 .: b3,(b6 .: b4,b5)
proof end;

theorem Th30: :: FINSEQOP:30
for b1 being non empty set
for b2, b3 being Element of b1
for b4 being Nat
for b5 being Element of b4 -tuples_on b1
for b6 being BinOp of b1 st b6 is associative holds
b6 [:] (b6 [;] b2,b5),b3 = b6 [;] b2,(b6 [:] b5,b3)
proof end;

theorem Th31: :: FINSEQOP:31
for b1 being non empty set
for b2 being Element of b1
for b3 being Nat
for b4, b5 being Element of b3 -tuples_on b1
for b6 being BinOp of b1 st b6 is associative holds
b6 .: (b6 [:] b4,b2),b5 = b6 .: b4,(b6 [;] b2,b5)
proof end;

theorem Th32: :: FINSEQOP:32
for b1 being non empty set
for b2, b3 being Element of b1
for b4 being Nat
for b5 being Element of b4 -tuples_on b1
for b6 being BinOp of b1 st b6 is associative holds
b6 [;] (b6 . b2,b3),b5 = b6 [;] b2,(b6 [;] b3,b5)
proof end;

theorem Th33: :: FINSEQOP:33
for b1 being non empty set
for b2, b3 being Element of b1
for b4 being Nat
for b5 being Element of b4 -tuples_on b1
for b6 being BinOp of b1 st b6 is associative holds
b6 [:] b5,(b6 . b2,b3) = b6 [:] (b6 [:] b5,b2),b3
proof end;

theorem Th34: :: FINSEQOP:34
for b1 being non empty set
for b2 being Nat
for b3, b4 being Element of b2 -tuples_on b1
for b5 being BinOp of b1 st b5 is commutative holds
b5 .: b3,b4 = b5 .: b4,b3
proof end;

theorem Th35: :: FINSEQOP:35
for b1 being non empty set
for b2 being Element of b1
for b3 being Nat
for b4 being Element of b3 -tuples_on b1
for b5 being BinOp of b1 st b5 is commutative holds
b5 [;] b2,b4 = b5 [:] b4,b2
proof end;

theorem Th36: :: FINSEQOP:36
for b1, b2 being non empty set
for b3, b4 being Element of b2
for b5 being Function of b1,b2
for b6, b7 being BinOp of b2 st b6 is_distributive_wrt b7 holds
b6 [;] (b7 . b3,b4),b5 = b7 .: (b6 [;] b3,b5),(b6 [;] b4,b5)
proof end;

theorem Th37: :: FINSEQOP:37
for b1, b2 being non empty set
for b3, b4 being Element of b2
for b5 being Function of b1,b2
for b6, b7 being BinOp of b2 st b6 is_distributive_wrt b7 holds
b6 [:] b5,(b7 . b3,b4) = b7 .: (b6 [:] b5,b3),(b6 [:] b5,b4)
proof end;

theorem Th38: :: FINSEQOP:38
for b1, b2, b3 being non empty set
for b4, b5 being Function of b1,b3
for b6 being Function of b3,b2
for b7 being BinOp of b3
for b8 being BinOp of b2 st ( for b9, b10 being Element of b3 holds b6 . (b7 . b9,b10) = b8 . (b6 . b9),(b6 . b10) ) holds
b6 * (b7 .: b4,b5) = b8 .: (b6 * b4),(b6 * b5)
proof end;

theorem Th39: :: FINSEQOP:39
for b1, b2, b3 being non empty set
for b4 being Element of b3
for b5 being Function of b1,b3
for b6 being Function of b3,b2
for b7 being BinOp of b3
for b8 being BinOp of b2 st ( for b9, b10 being Element of b3 holds b6 . (b7 . b9,b10) = b8 . (b6 . b9),(b6 . b10) ) holds
b6 * (b7 [;] b4,b5) = b8 [;] (b6 . b4),(b6 * b5)
proof end;

theorem Th40: :: FINSEQOP:40
for b1, b2, b3 being non empty set
for b4 being Element of b3
for b5 being Function of b1,b3
for b6 being Function of b3,b2
for b7 being BinOp of b3
for b8 being BinOp of b2 st ( for b9, b10 being Element of b3 holds b6 . (b7 . b9,b10) = b8 . (b6 . b9),(b6 . b10) ) holds
b6 * (b7 [:] b5,b4) = b8 [:] (b6 * b5),(b6 . b4)
proof end;

theorem Th41: :: FINSEQOP:41
for b1, b2 being non empty set
for b3, b4 being Function of b1,b2
for b5 being BinOp of b2
for b6 being UnOp of b2 st b6 is_distributive_wrt b5 holds
b6 * (b5 .: b3,b4) = b5 .: (b6 * b3),(b6 * b4)
proof end;

theorem Th42: :: FINSEQOP:42
for b1, b2 being non empty set
for b3 being Element of b2
for b4 being Function of b1,b2
for b5 being BinOp of b2
for b6 being UnOp of b2 st b6 is_distributive_wrt b5 holds
b6 * (b5 [;] b3,b4) = b5 [;] (b6 . b3),(b6 * b4)
proof end;

theorem Th43: :: FINSEQOP:43
for b1, b2 being non empty set
for b3 being Element of b2
for b4 being Function of b1,b2
for b5 being BinOp of b2
for b6 being UnOp of b2 st b6 is_distributive_wrt b5 holds
b6 * (b5 [:] b4,b3) = b5 [:] (b6 * b4),(b6 . b3)
proof end;

theorem Th44: :: FINSEQOP:44
for b1, b2 being non empty set
for b3 being Function of b2,b1
for b4 being BinOp of b1 st b4 has_a_unity holds
( b4 .: (b2 --> (the_unity_wrt b4)),b3 = b3 & b4 .: b3,(b2 --> (the_unity_wrt b4)) = b3 )
proof end;

theorem Th45: :: FINSEQOP:45
for b1, b2 being non empty set
for b3 being Function of b1,b2
for b4 being BinOp of b2 st b4 has_a_unity holds
b4 [;] (the_unity_wrt b4),b3 = b3
proof end;

theorem Th46: :: FINSEQOP:46
for b1, b2 being non empty set
for b3 being Function of b1,b2
for b4 being BinOp of b2 st b4 has_a_unity holds
b4 [:] b3,(the_unity_wrt b4) = b3
proof end;

theorem Th47: :: FINSEQOP:47
for b1 being non empty set
for b2, b3 being Element of b1
for b4 being Nat
for b5 being Element of b4 -tuples_on b1
for b6, b7 being BinOp of b1 st b6 is_distributive_wrt b7 holds
b6 [;] (b7 . b2,b3),b5 = b7 .: (b6 [;] b2,b5),(b6 [;] b3,b5)
proof end;

theorem Th48: :: FINSEQOP:48
for b1 being non empty set
for b2, b3 being Element of b1
for b4 being Nat
for b5 being Element of b4 -tuples_on b1
for b6, b7 being BinOp of b1 st b6 is_distributive_wrt b7 holds
b6 [:] b5,(b7 . b2,b3) = b7 .: (b6 [:] b5,b2),(b6 [:] b5,b3)
proof end;

theorem Th49: :: FINSEQOP:49
for b1, b2 being non empty set
for b3 being Nat
for b4 being Function of b2,b1
for b5, b6 being Element of b3 -tuples_on b2
for b7 being BinOp of b2
for b8 being BinOp of b1 st ( for b9, b10 being Element of b2 holds b4 . (b7 . b9,b10) = b8 . (b4 . b9),(b4 . b10) ) holds
b4 * (b7 .: b5,b6) = b8 .: (b4 * b5),(b4 * b6)
proof end;

theorem Th50: :: FINSEQOP:50
for b1, b2 being non empty set
for b3 being Element of b2
for b4 being Nat
for b5 being Function of b2,b1
for b6 being Element of b4 -tuples_on b2
for b7 being BinOp of b2
for b8 being BinOp of b1 st ( for b9, b10 being Element of b2 holds b5 . (b7 . b9,b10) = b8 . (b5 . b9),(b5 . b10) ) holds
b5 * (b7 [;] b3,b6) = b8 [;] (b5 . b3),(b5 * b6)
proof end;

theorem Th51: :: FINSEQOP:51
for b1, b2 being non empty set
for b3 being Element of b2
for b4 being Nat
for b5 being Function of b2,b1
for b6 being Element of b4 -tuples_on b2
for b7 being BinOp of b2
for b8 being BinOp of b1 st ( for b9, b10 being Element of b2 holds b5 . (b7 . b9,b10) = b8 . (b5 . b9),(b5 . b10) ) holds
b5 * (b7 [:] b6,b3) = b8 [:] (b5 * b6),(b5 . b3)
proof end;

theorem Th52: :: FINSEQOP:52
for b1 being non empty set
for b2 being Nat
for b3, b4 being Element of b2 -tuples_on b1
for b5 being BinOp of b1
for b6 being UnOp of b1 st b6 is_distributive_wrt b5 holds
b6 * (b5 .: b3,b4) = b5 .: (b6 * b3),(b6 * b4)
proof end;

theorem Th53: :: FINSEQOP:53
for b1 being non empty set
for b2 being Element of b1
for b3 being Nat
for b4 being Element of b3 -tuples_on b1
for b5 being BinOp of b1
for b6 being UnOp of b1 st b6 is_distributive_wrt b5 holds
b6 * (b5 [;] b2,b4) = b5 [;] (b6 . b2),(b6 * b4)
proof end;

theorem Th54: :: FINSEQOP:54
for b1 being non empty set
for b2 being Element of b1
for b3 being Nat
for b4 being Element of b3 -tuples_on b1
for b5 being BinOp of b1
for b6 being UnOp of b1 st b6 is_distributive_wrt b5 holds
b6 * (b5 [:] b4,b2) = b5 [:] (b6 * b4),(b6 . b2)
proof end;

theorem Th55: :: FINSEQOP:55
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being BinOp of b1
for b5 being UnOp of b1 st b3 is_distributive_wrt b4 & b5 = b3 [;] b2,(id b1) holds
b5 is_distributive_wrt b4
proof end;

theorem Th56: :: FINSEQOP:56
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being BinOp of b1
for b5 being UnOp of b1 st b3 is_distributive_wrt b4 & b5 = b3 [:] (id b1),b2 holds
b5 is_distributive_wrt b4
proof end;

theorem Th57: :: FINSEQOP:57
for b1 being non empty set
for b2 being Nat
for b3 being Element of b2 -tuples_on b1
for b4 being BinOp of b1 st b4 has_a_unity holds
( b4 .: (b2 |-> (the_unity_wrt b4)),b3 = b3 & b4 .: b3,(b2 |-> (the_unity_wrt b4)) = b3 )
proof end;

theorem Th58: :: FINSEQOP:58
for b1 being non empty set
for b2 being Nat
for b3 being Element of b2 -tuples_on b1
for b4 being BinOp of b1 st b4 has_a_unity holds
b4 [;] (the_unity_wrt b4),b3 = b3
proof end;

theorem Th59: :: FINSEQOP:59
for b1 being non empty set
for b2 being Nat
for b3 being Element of b2 -tuples_on b1
for b4 being BinOp of b1 st b4 has_a_unity holds
b4 [:] b3,(the_unity_wrt b4) = b3
proof end;

definition
let c1 be non empty set ;
let c2 be UnOp of c1;
let c3 be BinOp of c1;
pred c2 is_an_inverseOp_wrt c3 means :Def1: :: FINSEQOP:def 1
for b1 being Element of a1 holds
( a3 . b1,(a2 . b1) = the_unity_wrt a3 & a3 . (a2 . b1),b1 = the_unity_wrt a3 );
end;

:: deftheorem Def1 defines is_an_inverseOp_wrt FINSEQOP:def 1 :
for b1 being non empty set
for b2 being UnOp of b1
for b3 being BinOp of b1 holds
( b2 is_an_inverseOp_wrt b3 iff for b4 being Element of b1 holds
( b3 . b4,(b2 . b4) = the_unity_wrt b3 & b3 . (b2 . b4),b4 = the_unity_wrt b3 ) );

definition
let c1 be non empty set ;
let c2 be BinOp of c1;
attr a2 is having_an_inverseOp means :Def2: :: FINSEQOP:def 2
ex b1 being UnOp of a1 st b1 is_an_inverseOp_wrt a2;
end;

:: deftheorem Def2 defines having_an_inverseOp FINSEQOP:def 2 :
for b1 being non empty set
for b2 being BinOp of b1 holds
( b2 is having_an_inverseOp iff ex b3 being UnOp of b1 st b3 is_an_inverseOp_wrt b2 );

notation
let c1 be non empty set ;
let c2 be BinOp of c1;
synonym c2 has_an_inverseOp for having_an_inverseOp c2;
end;

definition
let c1 be non empty set ;
let c2 be BinOp of c1;
assume that
E30: c2 has_a_unity and
E31: c2 is associative and
E32: c2 has_an_inverseOp ;
func the_inverseOp_wrt c2 -> UnOp of a1 means :Def3: :: FINSEQOP:def 3
a3 is_an_inverseOp_wrt a2;
existence
ex b1 being UnOp of c1 st b1 is_an_inverseOp_wrt c2 by E32, Def2;
uniqueness
for b1, b2 being UnOp of c1 st b1 is_an_inverseOp_wrt c2 & b2 is_an_inverseOp_wrt c2 holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines the_inverseOp_wrt FINSEQOP:def 3 :
for b1 being non empty set
for b2 being BinOp of b1 st b2 has_a_unity & b2 is associative & b2 has_an_inverseOp holds
for b3 being UnOp of b1 holds
( b3 = the_inverseOp_wrt b2 iff b3 is_an_inverseOp_wrt b2 );

theorem Th60: :: FINSEQOP:60
canceled;

theorem Th61: :: FINSEQOP:61
canceled;

theorem Th62: :: FINSEQOP:62
canceled;

theorem Th63: :: FINSEQOP:63
for b1 being non empty set
for b2 being Element of b1
for b3 being BinOp of b1 st b3 has_a_unity & b3 is associative & b3 has_an_inverseOp holds
( b3 . ((the_inverseOp_wrt b3) . b2),b2 = the_unity_wrt b3 & b3 . b2,((the_inverseOp_wrt b3) . b2) = the_unity_wrt b3 )
proof end;

theorem Th64: :: FINSEQOP:64
for b1 being non empty set
for b2, b3 being Element of b1
for b4 being BinOp of b1 st b4 has_a_unity & b4 is associative & b4 has_an_inverseOp & b4 . b2,b3 = the_unity_wrt b4 holds
( b2 = (the_inverseOp_wrt b4) . b3 & (the_inverseOp_wrt b4) . b2 = b3 )
proof end;

theorem Th65: :: FINSEQOP:65
for b1 being non empty set
for b2 being BinOp of b1 st b2 has_a_unity & b2 is associative & b2 has_an_inverseOp holds
(the_inverseOp_wrt b2) . (the_unity_wrt b2) = the_unity_wrt b2
proof end;

theorem Th66: :: FINSEQOP:66
for b1 being non empty set
for b2 being Element of b1
for b3 being BinOp of b1 st b3 has_a_unity & b3 is associative & b3 has_an_inverseOp holds
(the_inverseOp_wrt b3) . ((the_inverseOp_wrt b3) . b2) = b2
proof end;

theorem Th67: :: FINSEQOP:67
for b1 being non empty set
for b2 being BinOp of b1 st b2 has_a_unity & b2 is associative & b2 is commutative & b2 has_an_inverseOp holds
the_inverseOp_wrt b2 is_distributive_wrt b2
proof end;

theorem Th68: :: FINSEQOP:68
for b1 being non empty set
for b2, b3, b4 being Element of b1
for b5 being BinOp of b1 st b5 has_a_unity & b5 is associative & b5 has_an_inverseOp & ( b5 . b2,b3 = b5 . b2,b4 or b5 . b3,b2 = b5 . b4,b2 ) holds
b3 = b4
proof end;

theorem Th69: :: FINSEQOP:69
for b1 being non empty set
for b2, b3 being Element of b1
for b4 being BinOp of b1 st b4 has_a_unity & b4 is associative & b4 has_an_inverseOp & ( b4 . b2,b3 = b3 or b4 . b3,b2 = b3 ) holds
b2 = the_unity_wrt b4
proof end;

theorem Th70: :: FINSEQOP:70
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being BinOp of b1 st b3 is associative & b3 has_a_unity & b3 has_an_inverseOp & b4 is_distributive_wrt b3 & b2 = the_unity_wrt b3 holds
for b5 being Element of b1 holds
( b4 . b2,b5 = b2 & b4 . b5,b2 = b2 )
proof end;

theorem Th71: :: FINSEQOP:71
for b1 being non empty set
for b2, b3 being Element of b1
for b4, b5 being BinOp of b1
for b6 being UnOp of b1 st b4 has_a_unity & b4 is associative & b4 has_an_inverseOp & b6 = the_inverseOp_wrt b4 & b5 is_distributive_wrt b4 holds
( b6 . (b5 . b2,b3) = b5 . (b6 . b2),b3 & b6 . (b5 . b2,b3) = b5 . b2,(b6 . b3) )
proof end;

theorem Th72: :: FINSEQOP:72
for b1 being non empty set
for b2, b3 being BinOp of b1
for b4 being UnOp of b1 st b2 has_a_unity & b2 is associative & b2 has_an_inverseOp & b4 = the_inverseOp_wrt b2 & b3 is_distributive_wrt b2 & b3 has_a_unity holds
b3 [;] (b4 . (the_unity_wrt b3)),(id b1) = b4
proof end;

theorem Th73: :: FINSEQOP:73
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being BinOp of b1 st b3 is associative & b3 has_a_unity & b3 has_an_inverseOp & b4 is_distributive_wrt b3 holds
(b4 [;] b2,(id b1)) . (the_unity_wrt b3) = the_unity_wrt b3
proof end;

theorem Th74: :: FINSEQOP:74
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being BinOp of b1 st b3 is associative & b3 has_a_unity & b3 has_an_inverseOp & b4 is_distributive_wrt b3 holds
(b4 [:] (id b1),b2) . (the_unity_wrt b3) = the_unity_wrt b3
proof end;

theorem Th75: :: FINSEQOP:75
for b1, b2 being non empty set
for b3 being Function of b2,b1
for b4 being BinOp of b1 st b4 has_a_unity & b4 is associative & b4 has_an_inverseOp holds
( b4 .: b3,((the_inverseOp_wrt b4) * b3) = b2 --> (the_unity_wrt b4) & b4 .: ((the_inverseOp_wrt b4) * b3),b3 = b2 --> (the_unity_wrt b4) )
proof end;

theorem Th76: :: FINSEQOP:76
for b1, b2 being non empty set
for b3, b4 being Function of b2,b1
for b5 being BinOp of b1 st b5 is associative & b5 has_an_inverseOp & b5 has_a_unity & b5 .: b3,b4 = b2 --> (the_unity_wrt b5) holds
( b3 = (the_inverseOp_wrt b5) * b4 & (the_inverseOp_wrt b5) * b3 = b4 )
proof end;

theorem Th77: :: FINSEQOP:77
for b1 being non empty set
for b2 being Nat
for b3 being Element of b2 -tuples_on b1
for b4 being BinOp of b1 st b4 has_a_unity & b4 is associative & b4 has_an_inverseOp holds
( b4 .: b3,((the_inverseOp_wrt b4) * b3) = b2 |-> (the_unity_wrt b4) & b4 .: ((the_inverseOp_wrt b4) * b3),b3 = b2 |-> (the_unity_wrt b4) )
proof end;

theorem Th78: :: FINSEQOP:78
for b1 being non empty set
for b2 being Nat
for b3, b4 being Element of b2 -tuples_on b1
for b5 being BinOp of b1 st b5 is associative & b5 has_an_inverseOp & b5 has_a_unity & b5 .: b3,b4 = b2 |-> (the_unity_wrt b5) holds
( b3 = (the_inverseOp_wrt b5) * b4 & (the_inverseOp_wrt b5) * b3 = b4 )
proof end;

theorem Th79: :: FINSEQOP:79
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being Function of b2,b1
for b5, b6 being BinOp of b1 st b5 is associative & b5 has_a_unity & b3 = the_unity_wrt b5 & b5 has_an_inverseOp & b6 is_distributive_wrt b5 holds
b6 [;] b3,b4 = b2 --> b3
proof end;

theorem Th80: :: FINSEQOP:80
for b1 being non empty set
for b2 being Element of b1
for b3 being Nat
for b4 being Element of b3 -tuples_on b1
for b5, b6 being BinOp of b1 st b5 is associative & b5 has_a_unity & b2 = the_unity_wrt b5 & b5 has_an_inverseOp & b6 is_distributive_wrt b5 holds
b6 [;] b2,b4 = b3 |-> b2
proof end;

definition
let c1, c2, c3 be Function;
func c1 * c2,c3 -> Function equals :: FINSEQOP:def 4
a1 * [:a2,a3:];
correctness
coherence
c1 * [:c2,c3:] is Function;
;
end;

:: deftheorem Def4 defines * FINSEQOP:def 4 :
for b1, b2, b3 being Function holds b1 * b2,b3 = b1 * [:b2,b3:];

theorem Th81: :: FINSEQOP:81
canceled;

theorem Th82: :: FINSEQOP:82
for b1, b2 being set
for b3, b4, b5 being Function st [b1,b2] in dom (b3 * b4,b5) holds
(b3 * b4,b5) . [b1,b2] = b3 . [(b4 . b1),(b5 . b2)]
proof end;

theorem Th83: :: FINSEQOP:83
for b1, b2 being set
for b3, b4, b5 being Function st [b1,b2] in dom (b3 * b4,b5) holds
(b3 * b4,b5) . b1,b2 = b3 . (b4 . b1),(b5 . b2) by Th82;

theorem Th84: :: FINSEQOP:84
for b1, b2, b3, b4, b5 being non empty set
for b6 being Function of [:b1,b2:],b3
for b7 being Function of b4,b1
for b8 being Function of b5,b2 holds b6 * b7,b8 is Function of [:b4,b5:],b3
proof end;

theorem Th85: :: FINSEQOP:85
for b1 being non empty set
for b2 being BinOp of b1
for b3, b4 being Function of b1,b1 holds b2 * b3,b4 is BinOp of b1 by Th84;

definition
let c1 be non empty set ;
let c2 be BinOp of c1;
let c3, c4 be Function of c1,c1;
redefine func * as c2 * c3,c4 -> BinOp of a1;
coherence
c2 * c3,c4 is BinOp of c1 by Th84;
end;

theorem Th86: :: FINSEQOP:86
for b1, b2, b3, b4, b5 being non empty set
for b6 being Element of b4
for b7 being Element of b5
for b8 being Function of [:b1,b2:],b3
for b9 being Function of b4,b1
for b10 being Function of b5,b2 holds (b8 * b9,b10) . b6,b7 = b8 . (b9 . b6),(b10 . b7)
proof end;

theorem Th87: :: FINSEQOP:87
for b1 being non empty set
for b2, b3 being Element of b1
for b4 being BinOp of b1
for b5 being Function of b1,b1 holds
( (b4 * (id b1),b5) . b2,b3 = b4 . b2,(b5 . b3) & (b4 * b5,(id b1)) . b2,b3 = b4 . (b5 . b2),b3 )
proof end;

theorem Th88: :: FINSEQOP:88
for b1, b2 being non empty set
for b3, b4 being Function of b1,b2
for b5 being BinOp of b2
for b6 being UnOp of b2 holds (b5 * (id b2),b6) .: b3,b4 = b5 .: b3,(b6 * b4)
proof end;

theorem Th89: :: FINSEQOP:89
for b1 being non empty set
for b2 being Nat
for b3, b4 being Element of b2 -tuples_on b1
for b5 being BinOp of b1
for b6 being UnOp of b1 holds (b5 * (id b1),b6) .: b3,b4 = b5 .: b3,(b6 * b4)
proof end;

theorem Th90: :: FINSEQOP:90
for b1 being non empty set
for b2, b3 being Element of b1
for b4 being BinOp of b1
for b5 being UnOp of b1 st b4 is associative & b4 has_a_unity & b4 is commutative & b4 has_an_inverseOp & b5 = the_inverseOp_wrt b4 holds
( b5 . ((b4 * (id b1),b5) . b2,b3) = (b4 * b5,(id b1)) . b2,b3 & (b4 * (id b1),b5) . b2,b3 = b5 . ((b4 * b5,(id b1)) . b2,b3) )
proof end;

theorem Th91: :: FINSEQOP:91
for b1 being non empty set
for b2 being Element of b1
for b3 being BinOp of b1 st b3 is associative & b3 has_a_unity & b3 has_an_inverseOp holds
(b3 * (id b1),(the_inverseOp_wrt b3)) . b2,b2 = the_unity_wrt b3
proof end;

theorem Th92: :: FINSEQOP:92
for b1 being non empty set
for b2 being Element of b1
for b3 being BinOp of b1 st b3 is associative & b3 has_a_unity & b3 has_an_inverseOp holds
(b3 * (id b1),(the_inverseOp_wrt b3)) . b2,(the_unity_wrt b3) = b2
proof end;

theorem Th93: :: FINSEQOP:93
for b1 being non empty set
for b2 being Element of b1
for b3 being BinOp of b1
for b4 being UnOp of b1 st b3 is associative & b3 has_a_unity & b3 has_an_inverseOp & b4 = the_inverseOp_wrt b3 holds
(b3 * (id b1),b4) . (the_unity_wrt b3),b2 = b4 . b2
proof end;

theorem Th94: :: FINSEQOP:94
for b1 being non empty set
for b2, b3 being BinOp of b1 st b2 is commutative & b2 is associative & b2 has_a_unity & b2 has_an_inverseOp & b3 = b2 * (id b1),(the_inverseOp_wrt b2) holds
for b4, b5, b6, b7 being Element of b1 holds b2 . (b3 . b4,b5),(b3 . b6,b7) = b3 . (b2 . b4,b6),(b2 . b5,b7)
proof end;