:: FINSOP_1 semantic presentation

definition

let c₁ be non empty set ;
let c₂ be Nat;
let c₃ be Element of c₁;
redefine func |-> as c₂ |-> c₃ -> FinSequence of a₁;
coherence by FINSEQ_2:77;

end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃ be BinOp of c₁;
assume E1: ( c₃ has_a_unity or len c₂ >= 1 ) ;
func c₃ "**" c₂ -> Element of a₁ means :Def1: :: FINSOP_1:def 1
a₄ = the_unity_wrt a₃ if ( a₃ has_a_unity & len a₂ = 0 )
otherwise ex b₁ being Function of NAT ,a₁ st
( b₁ . 1 = a₂ . 1 & ( for b₂ being Nat st 0 <> b₂ & b₂ < len a₂ holds
b₁ . (b₂ + 1) = a₃ . (b₁ . b₂),(a₂ . (b₂ + 1)) ) & a₄ = b₁ . (len a₂) );
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def1 defines "**" FINSOP_1:def 1 :

theorem Th1: :: FINSOP_1:1

canceled;

theorem Th2: :: FINSOP_1:2

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being BinOp of b₁ st len b₂ >= 1 holds
ex b₄ being Function of NAT ,b₁ st
( b₄ . 1 = b₂ . 1 & ( for b₅ being Nat st 0 <> b₅ & b₅ < len b₂ holds
b₄ . (b₅ + 1) = b₃ . (b₄ . b₅),(b₂ . (b₅ + 1)) ) & b₃ "**" b₂ = b₄ . (len b₂) ) by Def1;

theorem Th3: :: FINSOP_1:3

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁
for b₄ being BinOp of b₁ st len b₃ >= 1 & ex b₅ being Function of NAT ,b₁ st
( b₅ . 1 = b₃ . 1 & ( for b₆ being Nat st 0 <> b₆ & b₆ < len b₃ holds
b₅ . (b₆ + 1) = b₄ . (b₅ . b₆),(b₃ . (b₆ + 1)) ) & b₂ = b₅ . (len b₃) ) holds
b₂ = b₄ "**" b₃ by Def1;

definition

let c₁, c₂ be non empty set ;
let c₃ be Element of c₁;
redefine func --> as c₂ --> c₃ -> Function of a₂,a₁;
coherence by FUNCOP_1:58;

end;

definition

let c₁ be non empty set ;
let c₂ be Function of NAT ,c₁;
let c₃ be FinSequence of c₁;
redefine func +* as c₂ +* c₃ -> Function of NAT ,a₁;
coherence

proof end;

end;

definition

let c₁ be FinSequence;
redefine func dom as dom c₁ -> Element of Fin NAT ;
coherence

proof end;

end;

Lemma3: for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being BinOp of b₁ st len b₂ >= 1 & b₃ is associative & b₃ is commutative holds
b₃ "**" b₂ = b₃ $$ (dom b₂),((NAT --> (the_unity_wrt b₃)) +* b₂)

proof end;

Lemma4: for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being BinOp of b₁ st len b₂ = 0 & b₃ has_a_unity & b₃ is associative & b₃ is commutative holds
b₃ "**" b₂ = b₃ $$ (dom b₂),((NAT --> (the_unity_wrt b₃)) +* b₂)

proof end;

theorem Th4: :: FINSOP_1:4

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being BinOp of b₁ st ( b₃ has_a_unity or len b₂ >= 1 ) & b₃ is associative & b₃ is commutative holds
b₃ "**" b₂ = b₃ $$ (dom b₂),((NAT --> (the_unity_wrt b₃)) +* b₂)

proof end;

Lemma5: for b₁ being non empty set
for b₂ being BinOp of b₁ st b₂ has_a_unity holds
b₂ "**" (<*> b₁) = the_unity_wrt b₂

proof end;

Lemma6: for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being BinOp of b₁ holds b₃ "**" <*b₂*> = b₂

proof end;

Lemma7: for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁
for b₄ being BinOp of b₁ st len b₃ >= 1 holds
b₄ "**" (b₃ ^ <*b₂*>) = b₄ . (b₄ "**" b₃),b₂

proof end;

Lemma8: for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁
for b₄ being BinOp of b₁ st b₄ has_a_unity & len b₃ = 0 holds
b₄ "**" (b₃ ^ <*b₂*>) = b₄ . (b₄ "**" b₃),b₂

proof end;

theorem Th5: :: FINSOP_1:5

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁
for b₄ being BinOp of b₁ st ( b₄ has_a_unity or len b₃ >= 1 ) holds
b₄ "**" (b₃ ^ <*b₂*>) = b₄ . (b₄ "**" b₃),b₂

proof end;

theorem Th6: :: FINSOP_1:6

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄ being BinOp of b₁ st b₄ is associative & ( b₄ has_a_unity or ( len b₂ >= 1 & len b₃ >= 1 ) ) holds
b₄ "**" (b₂ ^ b₃) = b₄ . (b₄ "**" b₂),(b₄ "**" b₃)

proof end;

theorem Th7: :: FINSOP_1:7

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁
for b₄ being BinOp of b₁ st b₄ is associative & ( b₄ has_a_unity or len b₃ >= 1 ) holds
b₄ "**" (<*b₂*> ^ b₃) = b₄ . b₂,(b₄ "**" b₃)

proof end;

Lemma12: for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄ being BinOp of b₁ st b₄ is associative & b₄ is commutative holds
for b₅ being Permutation of dom b₂ st len b₂ >= 1 & len b₂ = len b₃ & ( for b₆ being Nat st b₆ in dom b₃ holds
b₃ . b₆ = b₂ . (b₅ . b₆) ) holds
b₄ "**" b₂ = b₄ "**" b₃

proof end;

Lemma13: for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄ being BinOp of b₁
for b₅ being Permutation of dom b₂ st b₄ has_a_unity & len b₂ = 0 & b₃ = b₂ * b₅ holds
b₄ "**" b₂ = b₄ "**" b₃

proof end;

theorem Th8: :: FINSOP_1:8

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄ being BinOp of b₁
for b₅ being Permutation of dom b₂ st b₄ is commutative & b₄ is associative & ( b₄ has_a_unity or len b₂ >= 1 ) & b₃ = b₂ * b₅ holds
b₄ "**" b₂ = b₄ "**" b₃

proof end;

Lemma15: for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄ being BinOp of b₁ st b₄ is associative & b₄ is commutative & b₂ is one-to-one & b₃ is one-to-one & rng b₂ = rng b₃ & len b₂ >= 1 holds
b₄ "**" b₂ = b₄ "**" b₃

proof end;

Lemma16: for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄ being BinOp of b₁ st len b₂ = 0 & b₄ has_a_unity & b₂ is one-to-one & b₃ is one-to-one & rng b₂ = rng b₃ holds
b₄ "**" b₂ = b₄ "**" b₃

proof end;

theorem Th9: :: FINSOP_1:9

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄ being BinOp of b₁ st ( b₄ has_a_unity or len b₂ >= 1 ) & b₄ is associative & b₄ is commutative & b₂ is one-to-one & b₃ is one-to-one & rng b₂ = rng b₃ holds
b₄ "**" b₂ = b₄ "**" b₃

proof end;

Lemma17: for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being BinOp of b₁ st len b₂ = 1 holds
b₃ "**" b₂ = b₂ . 1

proof end;

Lemma18: for b₁ being non empty set
for b₂, b₃, b₄ being FinSequence of b₁
for b₅ being BinOp of b₁ st b₅ is associative & b₅ is commutative & len b₂ >= 1 & len b₂ = len b₃ & len b₂ = len b₄ & ( for b₆ being Nat st b₆ in dom b₂ holds
b₄ . b₆ = b₅ . (b₂ . b₆),(b₃ . b₆) ) holds
b₅ "**" b₄ = b₅ . (b₅ "**" b₂),(b₅ "**" b₃)

proof end;

Lemma19: for b₁ being non empty set
for b₂, b₃, b₄ being FinSequence of b₁
for b₅ being BinOp of b₁ st b₅ has_a_unity & len b₂ = 0 & len b₂ = len b₃ & len b₂ = len b₄ holds
b₅ "**" b₂ = b₅ . (b₅ "**" b₃),(b₅ "**" b₄)

proof end;

theorem Th10: :: FINSOP_1:10

for b₁ being non empty set
for b₂, b₃, b₄ being FinSequence of b₁
for b₅ being BinOp of b₁ st b₅ is associative & b₅ is commutative & ( b₅ has_a_unity or len b₂ >= 1 ) & len b₂ = len b₃ & len b₂ = len b₄ & ( for b₆ being Nat st b₆ in dom b₂ holds
b₂ . b₆ = b₅ . (b₃ . b₆),(b₄ . b₆) ) holds
b₅ "**" b₂ = b₅ . (b₅ "**" b₃),(b₅ "**" b₄)

proof end;

theorem Th11: :: FINSOP_1:11

for b₁ being non empty set
for b₂ being BinOp of b₁ st b₂ has_a_unity holds
b₂ "**" (<*> b₁) = the_unity_wrt b₂ by Lemma5;

theorem Th12: :: FINSOP_1:12

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being BinOp of b₁ holds b₃ "**" <*b₂*> = b₂ by Lemma6;

theorem Th13: :: FINSOP_1:13

for b₁ being non empty set
for b₂, b₃ being Element of b₁
for b₄ being BinOp of b₁ holds b₄ "**" <*b₂,b₃*> = b₄ . b₂,b₃

proof end;

theorem Th14: :: FINSOP_1:14

for b₁ being non empty set
for b₂, b₃ being Element of b₁
for b₄ being BinOp of b₁ st b₄ is commutative holds
b₄ "**" <*b₂,b₃*> = b₄ "**" <*b₃,b₂*>

proof end;

theorem Th15: :: FINSOP_1:15

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁
for b₅ being BinOp of b₁ holds b₅ "**" <*b₂,b₃,b₄*> = b₅ . (b₅ . b₂,b₃),b₄

proof end;

theorem Th16: :: FINSOP_1:16

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁
for b₅ being BinOp of b₁ st b₅ is commutative holds
b₅ "**" <*b₂,b₃,b₄*> = b₅ "**" <*b₃,b₂,b₄*>

proof end;

theorem Th17: :: FINSOP_1:17

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being BinOp of b₁ holds b₃ "**" (1 |-> b₂) = b₂

proof end;

theorem Th18: :: FINSOP_1:18

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being BinOp of b₁ holds b₃ "**" (2 |-> b₂) = b₃ . b₂,b₂

proof end;

theorem Th19: :: FINSOP_1:19

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being BinOp of b₁
for b₄, b₅ being Nat st b₃ is associative & ( b₃ has_a_unity or ( b₄ <> 0 & b₅ <> 0 ) ) holds
b₃ "**" ((b₄ + b₅) |-> b₂) = b₃ . (b₃ "**" (b₄ |-> b₂)),(b₃ "**" (b₅ |-> b₂))

proof end;

theorem Th20: :: FINSOP_1:20

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being BinOp of b₁
for b₄, b₅ being Nat st b₃ is associative & ( b₃ has_a_unity or ( b₄ <> 0 & b₅ <> 0 ) ) holds
b₃ "**" ((b₄ * b₅) |-> b₂) = b₃ "**" (b₅ |-> (b₃ "**" (b₄ |-> b₂)))

proof end;

theorem Th21: :: FINSOP_1:21

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being BinOp of b₁ st len b₂ = 1 holds
b₃ "**" b₂ = b₂ . 1 by Lemma17;

theorem Th22: :: FINSOP_1:22

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being BinOp of b₁ st len b₂ = 2 holds
b₃ "**" b₂ = b₃ . (b₂ . 1),(b₂ . 2)

proof end;