:: by Czes{\l}aw Byli\'nski

::

:: Received May 4, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

:: Auxiliary theorems

theorem Th7: :: FINSEQOP:7

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))

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:70;

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

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:83;

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

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:77;

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

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:32;

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

theorem Th8: :: FINSEQOP:8

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)*>

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:9

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)

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 Th10: :: FINSEQOP:10

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))*>

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:11

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))

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 Th12: :: FINSEQOP:12

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))*>

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:13

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))

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 Th14: :: FINSEQOP:14

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))*>

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:15

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))

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:16

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)

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 Th17: :: FINSEQOP:17

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))

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

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

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:20

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)

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:21

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)

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:22

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

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:23

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

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 Th24: :: FINSEQOP:24

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)

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

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:26

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)

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

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:28

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)))

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:29

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)))

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:30

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)))

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:31

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)))

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

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:33

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)

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:34

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)

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 Th35: :: FINSEQOP:35

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)))

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

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 Th37: :: FINSEQOP:37

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))

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 Th38: :: FINSEQOP:38

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))

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

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:40

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))

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:41

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))

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

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 Th43: :: FINSEQOP:43

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 )

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 Th44: :: FINSEQOP:44

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

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

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:46

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)))

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

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 Th48: :: FINSEQOP:48

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))

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 Th49: :: FINSEQOP:49

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))

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

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:51

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))

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:52

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))

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

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:54

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

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: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 [:] ((id D),d) holds

u is_distributive_wrt F

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:56

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 )

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

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

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;

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

for d being Element of D holds

( F . (d,(u . d)) = the_unity_wrt F & F . ((u . d),d) = the_unity_wrt F );

:: 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 ) );

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;

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

ex u being UnOp of D st u is_an_inverseOp_wrt F;

:: 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 );

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 ;

existence

ex b_{1} being UnOp of D st b_{1} is_an_inverseOp_wrt F
by A3, Def2;

uniqueness

for b_{1}, b_{2} being UnOp of D st b_{1} is_an_inverseOp_wrt F & b_{2} is_an_inverseOp_wrt F holds

b_{1} = b_{2}

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

existence

ex b

uniqueness

for b

b

proof 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_{3} being UnOp of D holds

( b_{3} = the_inverseOp_wrt F iff b_{3} is_an_inverseOp_wrt F );

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

( b

theorem Th59: :: FINSEQOP:59

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 )

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 Th60: :: FINSEQOP:60

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 )

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 Th61: :: FINSEQOP:61

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

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 Th62: :: FINSEQOP:62

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

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 Th63: :: FINSEQOP:63

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

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 Th64: :: FINSEQOP:64

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

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 Th65: :: FINSEQOP:65

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

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 Th66: :: FINSEQOP:66

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 )

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 Th67: :: FINSEQOP:67

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)) )

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:68

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

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:69

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

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:70

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

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 Th71: :: FINSEQOP:71

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) )

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 Th72: :: FINSEQOP:72

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 )

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:73

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) )

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:74

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 )

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 Th75: :: FINSEQOP:75

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

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:76

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

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;

theorem Th77: :: FINSEQOP:77

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))

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:78

theorem Th79: :: FINSEQOP:79

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

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:80

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

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

theorem Th81: :: FINSEQOP:81

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))

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 Th82: :: FINSEQOP:82

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) )

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 Th83: :: FINSEQOP:83

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))

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:84

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))

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:85

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)) )

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:86

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

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:87

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

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:88

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

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:89

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)))

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;