:: SETWOP_2 semantic presentation

Lemma1: for b1 being Nat holds Seg b1 is Element of Fin NAT
by FINSUB_1:def 5;

E2: now
let c1 be Nat;
assume c1 + 1 in Seg c1 ;
then ( c1 + 1 <= c1 & c1 < c1 + 1 ) by FINSEQ_1:3, XREAL_1:31;
hence contradiction ;
end;

theorem Th1: :: SETWOP_2:1
canceled;

theorem Th2: :: SETWOP_2:2
canceled;

theorem Th3: :: SETWOP_2:3
for b1, b2 being non empty set
for b3, b4 being Element of b1
for b5 being BinOp of b2
for b6 being Function of b1,b2 st b5 is commutative & b5 is associative & b3 <> b4 holds
b5 $$ {b3,b4},b6 = b5 . (b6 . b3),(b6 . b4)
proof end;

theorem Th4: :: SETWOP_2:4
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being Element of Fin b1
for b5 being BinOp of b2
for b6 being Function of b1,b2 st b5 is commutative & b5 is associative & ( b4 <> {} or b5 has_a_unity ) & not b3 in b4 holds
b5 $$ (b4 \/ {b3}),b6 = b5 . (b5 $$ b4,b6),(b6 . b3)
proof end;

theorem Th5: :: SETWOP_2:5
for b1, b2 being non empty set
for b3, b4, b5 being Element of b1
for b6 being BinOp of b2
for b7 being Function of b1,b2 st b6 is commutative & b6 is associative & b3 <> b4 & b3 <> b5 & b4 <> b5 holds
b6 $$ {b3,b4,b5},b7 = b6 . (b6 . (b7 . b3),(b7 . b4)),(b7 . b5)
proof end;

theorem Th6: :: SETWOP_2:6
for b1, b2 being non empty set
for b3, b4 being Element of Fin b1
for b5 being BinOp of b2
for b6 being Function of b1,b2 st b5 is commutative & b5 is associative & ( ( b3 <> {} & b4 <> {} ) or b5 has_a_unity ) & b3 misses b4 holds
b5 $$ (b3 \/ b4),b6 = b5 . (b5 $$ b3,b6),(b5 $$ b4,b6)
proof end;

theorem Th7: :: SETWOP_2:7
for b1, b2, b3 being non empty set
for b4 being Element of Fin b1
for b5 being Element of Fin b2
for b6 being BinOp of b3
for b7 being Function of b1,b3
for b8 being Function of b2,b3 st b6 is commutative & b6 is associative & ( b5 <> {} or b6 has_a_unity ) & ex b9 being Function st
( dom b9 = b5 & rng b9 = b4 & b9 is one-to-one & b8 | b5 = b7 * b9 ) holds
b6 $$ b5,b8 = b6 $$ b4,b7
proof end;

theorem Th8: :: SETWOP_2:8
for b1, b2, b3 being non empty set
for b4 being Element of Fin b1
for b5 being Function of b1,b2
for b6 being BinOp of b3
for b7 being Function of b2,b3 st b6 is commutative & b6 is associative & ( b4 <> {} or b6 has_a_unity ) & b5 is one-to-one holds
b6 $$ (b5 .: b4),b7 = b6 $$ b4,(b7 * b5)
proof end;

theorem Th9: :: SETWOP_2:9
for b1, b2 being non empty set
for b3 being Element of Fin b1
for b4 being BinOp of b2
for b5, b6 being Function of b1,b2 st b4 is commutative & b4 is associative & ( b3 <> {} or b4 has_a_unity ) & b5 | b3 = b6 | b3 holds
b4 $$ b3,b5 = b4 $$ b3,b6
proof end;

theorem Th10: :: SETWOP_2:10
for b1, b2 being non empty set
for b3 being Element of Fin b1
for b4 being Element of b2
for b5 being BinOp of b2
for b6 being Function of b1,b2 st b5 is commutative & b5 is associative & b5 has_a_unity & b4 = the_unity_wrt b5 & b6 .: b3 = {b4} holds
b5 $$ b3,b6 = b4
proof end;

theorem Th11: :: SETWOP_2:11
for b1, b2 being non empty set
for b3 being Element of Fin b1
for b4 being Element of b2
for b5, b6 being BinOp of b2
for b7, b8 being Function of b1,b2 st b5 is commutative & b5 is associative & b5 has_a_unity & b4 = the_unity_wrt b5 & b6 . b4,b4 = b4 & ( for b9, b10, b11, b12 being Element of b2 holds b5 . (b6 . b9,b10),(b6 . b11,b12) = b6 . (b5 . b9,b11),(b5 . b10,b12) ) holds
b6 . (b5 $$ b3,b7),(b5 $$ b3,b8) = b5 $$ b3,(b6 .: b7,b8)
proof end;

Lemma7: for b1 being non empty set
for b2 being BinOp of b1 st b2 is commutative & b2 is associative holds
for b3, b4, b5, b6 being Element of b1 holds b2 . (b2 . b3,b4),(b2 . b5,b6) = b2 . (b2 . b3,b5),(b2 . b4,b6)
proof end;

theorem Th12: :: SETWOP_2:12
for b1, b2 being non empty set
for b3 being Element of Fin b1
for b4 being BinOp of b2
for b5, b6 being Function of b1,b2 st b4 is commutative & b4 is associative & b4 has_a_unity holds
b4 . (b4 $$ b3,b5),(b4 $$ b3,b6) = b4 $$ b3,(b4 .: b5,b6)
proof end;

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

theorem Th14: :: SETWOP_2:14
for b1, b2 being non empty set
for b3 being Element of Fin b1
for b4, b5 being Element of b2
for b6, b7 being BinOp of b2
for b8 being Function of b1,b2 st b6 is commutative & b6 is associative & b6 has_a_unity & b4 = the_unity_wrt b6 & b7 is_distributive_wrt b6 & b7 . b5,b4 = b4 holds
b7 . b5,(b6 $$ b3,b8) = b6 $$ b3,(b7 [;] b5,b8)
proof end;

theorem Th15: :: SETWOP_2:15
for b1, b2 being non empty set
for b3 being Element of Fin b1
for b4, b5 being Element of b2
for b6, b7 being BinOp of b2
for b8 being Function of b1,b2 st b6 is commutative & b6 is associative & b6 has_a_unity & b4 = the_unity_wrt b6 & b7 is_distributive_wrt b6 & b7 . b4,b5 = b4 holds
b7 . (b6 $$ b3,b8),b5 = b6 $$ b3,(b7 [:] b8,b5)
proof end;

theorem Th16: :: SETWOP_2:16
for b1, b2 being non empty set
for b3 being Element of Fin b1
for b4 being Element of b2
for b5, b6 being BinOp of b2
for b7 being Function of b1,b2 st b5 is commutative & b5 is associative & b5 has_a_unity & b5 has_an_inverseOp & b6 is_distributive_wrt b5 holds
b6 . b4,(b5 $$ b3,b7) = b5 $$ b3,(b6 [;] b4,b7)
proof end;

theorem Th17: :: SETWOP_2:17
for b1, b2 being non empty set
for b3 being Element of Fin b1
for b4 being Element of b2
for b5, b6 being BinOp of b2
for b7 being Function of b1,b2 st b5 is commutative & b5 is associative & b5 has_a_unity & b5 has_an_inverseOp & b6 is_distributive_wrt b5 holds
b6 . (b5 $$ b3,b7),b4 = b5 $$ b3,(b6 [:] b7,b4)
proof end;

theorem Th18: :: SETWOP_2:18
for b1, b2, b3 being non empty set
for b4 being Element of Fin b1
for b5 being BinOp of b3
for b6 being Function of b1,b3
for b7 being BinOp of b2
for b8 being Function of b3,b2 st b5 is commutative & b5 is associative & b5 has_a_unity & b7 is commutative & b7 is associative & b7 has_a_unity & b8 . (the_unity_wrt b5) = the_unity_wrt b7 & ( for b9, b10 being Element of b3 holds b8 . (b5 . b9,b10) = b7 . (b8 . b9),(b8 . b10) ) holds
b8 . (b5 $$ b4,b6) = b7 $$ b4,(b8 * b6)
proof end;

theorem Th19: :: SETWOP_2:19
for b1, b2 being non empty set
for b3 being Element of Fin b1
for b4 being BinOp of b2
for b5 being UnOp of b2
for b6 being Function of b1,b2 st b4 is commutative & b4 is associative & b4 has_a_unity & b5 . (the_unity_wrt b4) = the_unity_wrt b4 & b5 is_distributive_wrt b4 holds
b5 . (b4 $$ b3,b6) = b4 $$ b3,(b5 * b6)
proof end;

theorem Th20: :: SETWOP_2:20
for b1, b2 being non empty set
for b3 being Element of Fin b1
for b4 being Element of b2
for b5, b6 being BinOp of b2
for b7 being Function of b1,b2 st b5 is commutative & b5 is associative & b5 has_a_unity & b5 has_an_inverseOp & b6 is_distributive_wrt b5 holds
(b6 [;] b4,(id b2)) . (b5 $$ b3,b7) = b5 $$ b3,((b6 [;] b4,(id b2)) * b7)
proof end;

theorem Th21: :: SETWOP_2:21
for b1, b2 being non empty set
for b3 being Element of Fin b1
for b4 being BinOp of b2
for b5 being Function of b1,b2 st b4 is commutative & b4 is associative & b4 has_a_unity & b4 has_an_inverseOp holds
(the_inverseOp_wrt b4) . (b4 $$ b3,b5) = b4 $$ b3,((the_inverseOp_wrt b4) * b5)
proof end;

definition
let c1 be non empty set ;
let c2 be FinSequence of c1;
let c3 be Element of c1;
func [#] c2,c3 -> Function of NAT ,a1 equals :: SETWOP_2:def 1
(NAT --> a3) +* a2;
coherence
(NAT --> c3) +* c2 is Function of NAT ,c1 ;
end;

:: deftheorem Def1 defines [#] SETWOP_2:def 1 :
for b1 being non empty set
for b2 being FinSequence of b1
for b3 being Element of b1 holds [#] b2,b3 = (NAT --> b3) +* b2;

theorem Th22: :: SETWOP_2:22
for b1 being non empty set
for b2 being Element of b1
for b3 being Nat
for b4 being FinSequence of b1 holds
( ( b3 in dom b4 implies ([#] b4,b2) . b3 = b4 . b3 ) & ( not b3 in dom b4 implies ([#] b4,b2) . b3 = b2 ) )
proof end;

theorem Th23: :: SETWOP_2:23
for b1 being non empty set
for b2 being Element of b1
for b3 being FinSequence of b1 holds ([#] b3,b2) | (dom b3) = b3
proof end;

theorem Th24: :: SETWOP_2:24
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being FinSequence of b1 holds ([#] (b3 ^ b4),b2) | (dom b3) = b3
proof end;

theorem Th25: :: SETWOP_2:25
for b1 being non empty set
for b2 being Element of b1
for b3 being FinSequence of b1 holds rng ([#] b3,b2) = (rng b3) \/ {b2}
proof end;

theorem Th26: :: SETWOP_2:26
for b1, b2 being non empty set
for b3 being Element of b2
for b4 being Function of b2,b1
for b5 being FinSequence of b2 holds b4 * ([#] b5,b3) = [#] (b4 * b5),(b4 . b3)
proof end;

Lemma12: for b1 being non empty set
for b2 being Element of b1
for b3 being BinOp of b1
for b4, b5 being FinSequence of b1 st len b4 = len b5 & b3 . b2,b2 = b2 holds
b3 .: ([#] b4,b2),([#] b5,b2) = [#] (b3 .: b4,b5),b2
proof end;

Lemma13: for b1 being non empty set
for b2, b3 being Element of b1
for b4 being BinOp of b1
for b5 being FinSequence of b1 st b4 . b2,b3 = b2 holds
b4 [:] ([#] b5,b2),b3 = [#] (b4 [:] b5,b3),b2
proof end;

Lemma14: for b1 being non empty set
for b2, b3 being Element of b1
for b4 being BinOp of b1
for b5 being FinSequence of b1 st b4 . b2,b3 = b3 holds
b4 [;] b2,([#] b5,b3) = [#] (b4 [;] b2,b5),b3
proof end;

definition
let c1 be Nat;
redefine func Seg as Seg c1 -> Element of Fin NAT ;
coherence
Seg c1 is Element of Fin NAT by Lemma1;
end;

definition
let c1 be FinSequence;
redefine func dom as dom c1 -> Element of Fin NAT ;
coherence
dom c1 is Element of Fin NAT
proof end;
end;

notation
let c1 be non empty set ;
let c2 be FinSequence of c1;
let c3 be BinOp of c1;
synonym c3 $$ c2 for c3 "**" c2;
end;

definition
let c1 be non empty set ;
let c2 be FinSequence of c1;
let c3 be BinOp of c1;
assume E15: ( ( c3 has_a_unity or len c2 >= 1 ) & c3 is associative & c3 is commutative ) ;
redefine func c3 "**" c2 -> Element of a1 equals :Def2: :: SETWOP_2:def 2
a3 $$ (dom a2),([#] a2,(the_unity_wrt a3));
compatibility
for b1 being Element of c1 holds
( b1 = c3 $$ c2 iff b1 = c3 $$ (dom c2),([#] c2,(the_unity_wrt c3)) ) by E15, FINSOP_1:4;
end;

:: deftheorem Def2 defines $$ SETWOP_2:def 2 :
for b1 being non empty set
for b2 being FinSequence of b1
for b3 being BinOp of b1 st ( b3 has_a_unity or len b2 >= 1 ) & b3 is associative & b3 is commutative holds
b3 $$ b2 = b3 $$ (dom b2),([#] b2,(the_unity_wrt b3));

theorem Th27: :: SETWOP_2:27
canceled;

theorem Th28: :: SETWOP_2:28
canceled;

theorem Th29: :: SETWOP_2:29
canceled;

theorem Th30: :: SETWOP_2:30
canceled;

theorem Th31: :: SETWOP_2:31
canceled;

theorem Th32: :: SETWOP_2:32
canceled;

theorem Th33: :: SETWOP_2:33
canceled;

theorem Th34: :: SETWOP_2:34
canceled;

theorem Th35: :: SETWOP_2:35
for b1 being non empty set
for b2 being BinOp of b1
for b3 being Nat st b2 has_a_unity holds
b2 "**" (b3 |-> (the_unity_wrt b2)) = the_unity_wrt b2
proof end;

theorem Th36: :: SETWOP_2:36
canceled;

theorem Th37: :: SETWOP_2:37
for b1 being non empty set
for b2 being Element of b1
for b3 being BinOp of b1
for b4, b5 being Nat st b3 is associative & ( ( b4 >= 1 & b5 >= 1 ) or b3 has_a_unity ) holds
b3 "**" ((b4 + b5) |-> b2) = b3 . (b3 "**" (b4 |-> b2)),(b3 "**" (b5 |-> b2))
proof end;

theorem Th38: :: SETWOP_2:38
for b1 being non empty set
for b2 being Element of b1
for b3 being BinOp of b1
for b4, b5 being Nat st b3 is commutative & b3 is associative & ( ( b4 >= 1 & b5 >= 1 ) or b3 has_a_unity ) holds
b3 "**" ((b4 * b5) |-> b2) = b3 "**" (b5 |-> (b3 "**" (b4 |-> b2)))
proof end;

theorem Th39: :: SETWOP_2:39
for b1, b2 being non empty set
for b3 being BinOp of b2
for b4 being BinOp of b1
for b5 being Function of b2,b1
for b6 being FinSequence of b2 st b3 has_a_unity & b4 has_a_unity & b5 . (the_unity_wrt b3) = the_unity_wrt b4 & ( for b7, b8 being Element of b2 holds b5 . (b3 . b7,b8) = b4 . (b5 . b7),(b5 . b8) ) holds
b5 . (b3 "**" b6) = b4 "**" (b5 * b6)
proof end;

theorem Th40: :: SETWOP_2:40
for b1 being non empty set
for b2 being BinOp of b1
for b3 being UnOp of b1
for b4 being FinSequence of b1 st b2 has_a_unity & b3 . (the_unity_wrt b2) = the_unity_wrt b2 & b3 is_distributive_wrt b2 holds
b3 . (b2 "**" b4) = b2 "**" (b3 * b4)
proof end;

theorem Th41: :: SETWOP_2:41
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being BinOp of b1
for b5 being FinSequence of b1 st b3 is associative & b3 has_a_unity & b3 has_an_inverseOp & b4 is_distributive_wrt b3 holds
(b4 [;] b2,(id b1)) . (b3 "**" b5) = b3 "**" ((b4 [;] b2,(id b1)) * b5)
proof end;

theorem Th42: :: SETWOP_2:42
for b1 being non empty set
for b2 being BinOp of b1
for b3 being FinSequence of b1 st b2 is commutative & b2 is associative & b2 has_a_unity & b2 has_an_inverseOp holds
(the_inverseOp_wrt b2) . (b2 "**" b3) = b2 "**" ((the_inverseOp_wrt b2) * b3)
proof end;

theorem Th43: :: SETWOP_2:43
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being BinOp of b1
for b5, b6 being FinSequence of b1 st b3 is commutative & b3 is associative & b3 has_a_unity & b2 = the_unity_wrt b3 & b4 . b2,b2 = b2 & ( for b7, b8, b9, b10 being Element of b1 holds b3 . (b4 . b7,b8),(b4 . b9,b10) = b4 . (b3 . b7,b9),(b3 . b8,b10) ) & len b5 = len b6 holds
b4 . (b3 "**" b5),(b3 "**" b6) = b3 "**" (b4 .: b5,b6)
proof end;

theorem Th44: :: SETWOP_2:44
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being BinOp of b1
for b5 being Nat
for b6, b7 being Element of b5 -tuples_on b1 st b3 is commutative & b3 is associative & b3 has_a_unity & b2 = the_unity_wrt b3 & b4 . b2,b2 = b2 & ( for b8, b9, b10, b11 being Element of b1 holds b3 . (b4 . b8,b9),(b4 . b10,b11) = b4 . (b3 . b8,b10),(b3 . b9,b11) ) holds
b4 . (b3 "**" b6),(b3 "**" b7) = b3 "**" (b4 .: b6,b7)
proof end;

theorem Th45: :: SETWOP_2:45
for b1 being non empty set
for b2 being BinOp of b1
for b3, b4 being FinSequence of b1 st b2 is commutative & b2 is associative & b2 has_a_unity & len b3 = len b4 holds
b2 . (b2 "**" b3),(b2 "**" b4) = b2 "**" (b2 .: b3,b4)
proof end;

theorem Th46: :: SETWOP_2:46
for b1 being non empty set
for b2 being BinOp of b1
for b3 being Nat
for b4, b5 being Element of b3 -tuples_on b1 st b2 is commutative & b2 is associative & b2 has_a_unity holds
b2 . (b2 "**" b4),(b2 "**" b5) = b2 "**" (b2 .: b4,b5)
proof end;

theorem Th47: :: SETWOP_2:47
for b1 being non empty set
for b2, b3 being Element of b1
for b4 being BinOp of b1
for b5 being Nat st b4 is commutative & b4 is associative & b4 has_a_unity holds
b4 "**" (b5 |-> (b4 . b2,b3)) = b4 . (b4 "**" (b5 |-> b2)),(b4 "**" (b5 |-> b3))
proof end;

theorem Th48: :: SETWOP_2:48
for b1 being non empty set
for b2, b3 being BinOp of b1
for b4 being Nat
for b5, b6 being Element of b4 -tuples_on 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
b3 . (b2 "**" b5),(b2 "**" b6) = b2 "**" (b3 .: b5,b6)
proof end;

theorem Th49: :: SETWOP_2:49
for b1 being non empty set
for b2, b3 being Element of b1
for b4, b5 being BinOp of b1
for b6 being FinSequence of b1 st b4 is commutative & b4 is associative & b4 has_a_unity & b2 = the_unity_wrt b4 & b5 is_distributive_wrt b4 & b5 . b3,b2 = b2 holds
b5 . b3,(b4 "**" b6) = b4 "**" (b5 [;] b3,b6)
proof end;

theorem Th50: :: SETWOP_2:50
for b1 being non empty set
for b2, b3 being Element of b1
for b4, b5 being BinOp of b1
for b6 being FinSequence of b1 st b4 is commutative & b4 is associative & b4 has_a_unity & b2 = the_unity_wrt b4 & b5 is_distributive_wrt b4 & b5 . b2,b3 = b2 holds
b5 . (b4 "**" b6),b3 = b4 "**" (b5 [:] b6,b3)
proof end;

theorem Th51: :: SETWOP_2:51
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being BinOp of b1
for b5 being FinSequence of b1 st b3 is commutative & b3 is associative & b3 has_a_unity & b3 has_an_inverseOp & b4 is_distributive_wrt b3 holds
b4 . b2,(b3 "**" b5) = b3 "**" (b4 [;] b2,b5)
proof end;

theorem Th52: :: SETWOP_2:52
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being BinOp of b1
for b5 being FinSequence of b1 st b3 is commutative & b3 is associative & b3 has_a_unity & b3 has_an_inverseOp & b4 is_distributive_wrt b3 holds
b4 . (b3 "**" b5),b2 = b3 "**" (b4 [:] b5,b2)
proof end;