:: FINSEQOP semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: FINSEQOP:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function holds
( <:{} ,f:> = {} & <:f,{} :> = {} )
proof end;

theorem :: FINSEQOP:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function holds
( [:{} ,f:] = {} & [:f,{} :] = {} )
proof end;

theorem :: FINSEQOP:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: FINSEQOP:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, f being Function holds
( F .: {} ,f = {} & F .: f,{} = {} )
proof end;

theorem :: FINSEQOP:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for F being Function holds F [:] {} ,x = {}
proof end;

theorem :: FINSEQOP:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for F being Function holds F [;] x,{} = {}
proof end;

theorem Th7: :: FINSEQOP:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x1, x2 being set holds <:(X --> x1),(X --> x2):> = X --> [x1,x2]
proof end;

theorem Th8: :: FINSEQOP:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Function
for X, x1, x2 being set st [x1,x2] in dom F holds
F .: (X --> x1),(X --> x2) = X --> (F . [x1,x2])
proof end;

definition
let D, D', E be non empty set ;
let F be Function of [:D,D':],E;
let p be FinSequence of D;
let p' be FinSequence of D';
:: original: .:
redefine func F .: p,p' -> FinSequence of E;
coherence
F .: p,p' is FinSequence of E
by FINSEQ_2:84;
end;

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

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

definition
let D be non empty set ;
let i be Nat;
let d be Element of D;
:: original: |->
redefine func i |-> d -> Element of i -tuples_on D;
coherence
i |-> d is Element of i -tuples_on D
by FINSEQ_2:132;
end;

definition
let D, E be set ;
let p be FinSequence of D;
let h be Function of D,E;
:: original: *
redefine func h * p -> FinSequence of E;
coherence
p * h is FinSequence of E
by FINSEQ_2:36;
end;

theorem Th9: :: FINSEQOP:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, E being non empty set
for d being Element of D
for p being FinSequence of D
for h being Function of D,E holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>
proof end;

theorem :: FINSEQOP:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, E being non empty set
for p, q being FinSequence of D
for h being Function of D,E holds h * (p ^ q) = (h * p) ^ (h * q)
proof end;

Lm1: for C, D being non empty set
for f being Function of C,D
for T being Element of 0 -tuples_on C holds f * T = <*> D
proof end;

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

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

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

theorem Th11: :: FINSEQOP:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E, D, D' being non empty set
for d being Element of D
for d' being Element of D'
for i being Nat
for F being Function of [:D,D':],E
for T being Element of i -tuples_on D
for T' being Element of i -tuples_on D' holds F .: (T ^ <*d*>),(T' ^ <*d'*>) = (F .: T,T') ^ <*(F . d,d')*>
proof end;

theorem :: FINSEQOP:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E, D, D' being non empty set
for i, j being Nat
for F being Function of [:D,D':],E
for T being Element of i -tuples_on D
for T' being Element of i -tuples_on D'
for S being Element of j -tuples_on D
for S' being Element of j -tuples_on D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
proof end;

theorem Th13: :: FINSEQOP:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, E, D' being non empty set
for d being Element of D
for d' being Element of D'
for F being Function of [:D,D':],E
for p' being FinSequence of D' holds F [;] d,(p' ^ <*d'*>) = (F [;] d,p') ^ <*(F . d,d')*>
proof end;

theorem :: FINSEQOP:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, E, D' being non empty set
for d being Element of D
for F being Function of [:D,D':],E
for p', q' being FinSequence of D' holds F [;] d,(p' ^ q') = (F [;] d,p') ^ (F [;] d,q')
proof end;

theorem Th15: :: FINSEQOP:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D', E, D being non empty set
for d being Element of D
for d' being Element of D'
for F being Function of [:D,D':],E
for p being FinSequence of D holds F [:] (p ^ <*d*>),d' = (F [:] p,d') ^ <*(F . d,d')*>
proof end;

theorem :: FINSEQOP:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D', E, D being non empty set
for d' being Element of D'
for F being Function of [:D,D':],E
for p, q being FinSequence of D holds F [:] (p ^ q),d' = (F [:] p,d') ^ (F [:] q,d')
proof end;

theorem :: FINSEQOP:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, E being non empty set
for d being Element of D
for i being Nat
for h being Function of D,E holds h * (i |-> d) = i |-> (h . d)
proof end;

theorem Th18: :: FINSEQOP:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, D', E being non empty set
for d being Element of D
for d' being Element of D'
for i being Nat
for F being Function of [:D,D':],E holds F .: (i |-> d),(i |-> d') = i |-> (F . d,d')
proof end;

theorem :: FINSEQOP:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, D', E being non empty set
for d being Element of D
for d' being Element of D'
for i being Nat
for F being Function of [:D,D':],E holds F [;] d,(i |-> d') = i |-> (F . d,d')
proof end;

theorem :: FINSEQOP:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, D', E being non empty set
for d being Element of D
for d' being Element of D'
for i being Nat
for F being Function of [:D,D':],E holds F [:] (i |-> d),d' = i |-> (F . d,d')
proof end;

theorem :: FINSEQOP:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, E, D' being non empty set
for d being Element of D
for i being Nat
for F being Function of [:D,D':],E
for T' being Element of i -tuples_on D' holds F .: (i |-> d),T' = F [;] d,T'
proof end;

theorem :: FINSEQOP:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D', E, D being non empty set
for d being Element of D
for i being Nat
for F being Function of [:D,D':],E
for T being Element of i -tuples_on D holds F .: T,(i |-> d) = F [:] T,d
proof end;

theorem :: FINSEQOP:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, E, D' being non empty set
for d being Element of D
for i being Nat
for F being Function of [:D,D':],E
for T' being Element of i -tuples_on D' holds F [;] d,T' = (F [;] d,(id D')) * T'
proof end;

theorem :: FINSEQOP:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D', E, D being non empty set
for d being Element of D
for i being Nat
for F being Function of [:D,D':],E
for T being Element of i -tuples_on D holds F [:] T,d = (F [:] (id D),d) * T
proof end;

Lm5: for D being non empty set
for i being Nat
for T being Element of i -tuples_on D holds T is Function of Seg i,D
proof end;

theorem Th25: :: FINSEQOP:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being non empty set
for d being Element of D
for f, f' being Function of C,D
for F being BinOp of D st F is associative holds
(F [;] d,(id D)) * (F .: f,f') = F .: ((F [;] d,(id D)) * f),f'
proof end;

theorem Th26: :: FINSEQOP:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being non empty set
for d being Element of D
for f, f' being Function of C,D
for F being BinOp of D st F is associative holds
(F [:] (id D),d) * (F .: f,f') = F .: f,((F [:] (id D),d) * f')
proof end;

theorem :: FINSEQOP:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for i being Nat
for T1, T2 being Element of i -tuples_on D
for F being BinOp of D st F is associative holds
(F [;] d,(id D)) * (F .: T1,T2) = F .: ((F [;] d,(id D)) * T1),T2
proof end;

theorem :: FINSEQOP:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for i being Nat
for T1, T2 being Element of i -tuples_on D
for F being BinOp of D st F is associative holds
(F [:] (id D),d) * (F .: T1,T2) = F .: T1,((F [:] (id D),d) * T2)
proof end;

theorem :: FINSEQOP:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for i being Nat
for T1, T2, T3 being Element of i -tuples_on D
for F being BinOp of D st F is associative holds
F .: (F .: T1,T2),T3 = F .: T1,(F .: T2,T3)
proof end;

theorem :: FINSEQOP:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d1, d2 being Element of D
for i being Nat
for T being Element of i -tuples_on D
for F being BinOp of D st F is associative holds
F [:] (F [;] d1,T),d2 = F [;] d1,(F [:] T,d2)
proof end;

theorem :: FINSEQOP:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for i being Nat
for T1, T2 being Element of i -tuples_on D
for F being BinOp of D st F is associative holds
F .: (F [:] T1,d),T2 = F .: T1,(F [;] d,T2)
proof end;

theorem :: FINSEQOP:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d1, d2 being Element of D
for i being Nat
for T being Element of i -tuples_on D
for F being BinOp of D st F is associative holds
F [;] (F . d1,d2),T = F [;] d1,(F [;] d2,T)
proof end;

theorem :: FINSEQOP:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d1, d2 being Element of D
for i being Nat
for T being Element of i -tuples_on D
for F being BinOp of D st F is associative holds
F [:] T,(F . d1,d2) = F [:] (F [:] T,d1),d2
proof end;

theorem :: FINSEQOP:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for i being Nat
for T1, T2 being Element of i -tuples_on D
for F being BinOp of D st F is commutative holds
F .: T1,T2 = F .: T2,T1
proof end;

theorem :: FINSEQOP:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for i being Nat
for T being Element of i -tuples_on D
for F being BinOp of D st F is commutative holds
F [;] d,T = F [:] T,d
proof end;

theorem Th36: :: FINSEQOP:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being non empty set
for d1, d2 being Element of D
for f being Function of C,D
for F, G being BinOp of D st F is_distributive_wrt G holds
F [;] (G . d1,d2),f = G .: (F [;] d1,f),(F [;] d2,f)
proof end;

theorem Th37: :: FINSEQOP:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being non empty set
for d1, d2 being Element of D
for f being Function of C,D
for F, G being BinOp of D st F is_distributive_wrt G holds
F [:] f,(G . d1,d2) = G .: (F [:] f,d1),(F [:] f,d2)
proof end;

theorem Th38: :: FINSEQOP:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, E, D being non empty set
for f, f' being Function of C,D
for h being Function of D,E
for F being BinOp of D
for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . d1,d2) = H . (h . d1),(h . d2) ) holds
h * (F .: f,f') = H .: (h * f),(h * f')
proof end;

theorem Th39: :: FINSEQOP:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, E, D being non empty set
for d being Element of D
for f being Function of C,D
for h being Function of D,E
for F being BinOp of D
for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . d1,d2) = H . (h . d1),(h . d2) ) holds
h * (F [;] d,f) = H [;] (h . d),(h * f)
proof end;

theorem Th40: :: FINSEQOP:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, E, D being non empty set
for d being Element of D
for f being Function of C,D
for h being Function of D,E
for F being BinOp of D
for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . d1,d2) = H . (h . d1),(h . d2) ) holds
h * (F [:] f,d) = H [:] (h * f),(h . d)
proof end;

theorem :: FINSEQOP:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being non empty set
for f, f' being Function of C,D
for F being BinOp of D
for u being UnOp of D st u is_distributive_wrt F holds
u * (F .: f,f') = F .: (u * f),(u * f')
proof end;

theorem :: FINSEQOP:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being non empty set
for d being Element of D
for f being Function of C,D
for F being BinOp of D
for u being UnOp of D st u is_distributive_wrt F holds
u * (F [;] d,f) = F [;] (u . d),(u * f)
proof end;

theorem :: FINSEQOP:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being non empty set
for d being Element of D
for f being Function of C,D
for F being BinOp of D
for u being UnOp of D st u is_distributive_wrt F holds
u * (F [:] f,d) = F [:] (u * f),(u . d)
proof end;

theorem Th44: :: FINSEQOP:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, C being non empty set
for f being Function of C,D
for F being BinOp of D st F has_a_unity holds
( F .: (C --> (the_unity_wrt F)),f = f & F .: f,(C --> (the_unity_wrt F)) = f )
proof end;

theorem Th45: :: FINSEQOP:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being non empty set
for f being Function of C,D
for F being BinOp of D st F has_a_unity holds
F [;] (the_unity_wrt F),f = f
proof end;

theorem Th46: :: FINSEQOP:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being non empty set
for f being Function of C,D
for F being BinOp of D st F has_a_unity holds
F [:] f,(the_unity_wrt F) = f
proof end;

theorem :: FINSEQOP:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d1, d2 being Element of D
for i being Nat
for T being Element of i -tuples_on D
for F, G being BinOp of D st F is_distributive_wrt G holds
F [;] (G . d1,d2),T = G .: (F [;] d1,T),(F [;] d2,T)
proof end;

theorem :: FINSEQOP:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d1, d2 being Element of D
for i being Nat
for T being Element of i -tuples_on D
for F, G being BinOp of D st F is_distributive_wrt G holds
F [:] T,(G . d1,d2) = G .: (F [:] T,d1),(F [:] T,d2)
proof end;

theorem Th49: :: FINSEQOP:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E, D being non empty set
for i being Nat
for h being Function of D,E
for T1, T2 being Element of i -tuples_on D
for F being BinOp of D
for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . d1,d2) = H . (h . d1),(h . d2) ) holds
h * (F .: T1,T2) = H .: (h * T1),(h * T2)
proof end;

theorem Th50: :: FINSEQOP:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E, D being non empty set
for d being Element of D
for i being Nat
for h being Function of D,E
for T being Element of i -tuples_on D
for F being BinOp of D
for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . d1,d2) = H . (h . d1),(h . d2) ) holds
h * (F [;] d,T) = H [;] (h . d),(h * T)
proof end;

theorem Th51: :: FINSEQOP:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E, D being non empty set
for d being Element of D
for i being Nat
for h being Function of D,E
for T being Element of i -tuples_on D
for F being BinOp of D
for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . d1,d2) = H . (h . d1),(h . d2) ) holds
h * (F [:] T,d) = H [:] (h * T),(h . d)
proof end;

theorem :: FINSEQOP:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for i being Nat
for T1, T2 being Element of i -tuples_on D
for F being BinOp of D
for u being UnOp of D st u is_distributive_wrt F holds
u * (F .: T1,T2) = F .: (u * T1),(u * T2)
proof end;

theorem :: FINSEQOP:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for i being Nat
for T being Element of i -tuples_on D
for F being BinOp of D
for u being UnOp of D st u is_distributive_wrt F holds
u * (F [;] d,T) = F [;] (u . d),(u * T)
proof end;

theorem :: FINSEQOP:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for i being Nat
for T being Element of i -tuples_on D
for F being BinOp of D
for u being UnOp of D st u is_distributive_wrt F holds
u * (F [:] T,d) = F [:] (u * T),(u . d)
proof end;

theorem :: FINSEQOP:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for G, F being BinOp of D
for u being UnOp of D st G is_distributive_wrt F & u = G [;] d,(id D) holds
u is_distributive_wrt F
proof end;

theorem :: FINSEQOP:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for G, F being BinOp of D
for u being UnOp of D st G is_distributive_wrt F & u = G [:] (id D),d holds
u is_distributive_wrt F
proof end;

theorem :: FINSEQOP:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for i being Nat
for T being Element of i -tuples_on D
for F being BinOp of D st F has_a_unity holds
( F .: (i |-> (the_unity_wrt F)),T = T & F .: T,(i |-> (the_unity_wrt F)) = T )
proof end;

theorem :: FINSEQOP:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for i being Nat
for T being Element of i -tuples_on D
for F being BinOp of D st F has_a_unity holds
F [;] (the_unity_wrt F),T = T
proof end;

theorem :: FINSEQOP:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for i being Nat
for T being Element of i -tuples_on D
for F being BinOp of D st F has_a_unity holds
F [:] T,(the_unity_wrt F) = T
proof end;

definition
let D be non empty set ;
let u be UnOp of D;
let F be BinOp of D;
pred u is_an_inverseOp_wrt F means :Def1: :: FINSEQOP:def 1
for d being Element of D holds
( F . d,(u . d) = the_unity_wrt F & F . (u . d),d = the_unity_wrt F );
end;

:: deftheorem Def1 defines is_an_inverseOp_wrt FINSEQOP:def 1 :
for D being non empty set
for u being UnOp of D
for F being BinOp of D holds
( u is_an_inverseOp_wrt F iff for d being Element of D holds
( F . d,(u . d) = the_unity_wrt F & F . (u . d),d = the_unity_wrt F ) );

definition
let D be non empty set ;
let F be BinOp of D;
attr F is having_an_inverseOp means :Def2: :: FINSEQOP:def 2
ex u being UnOp of D st u is_an_inverseOp_wrt F;
end;

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

notation
let D be non empty set ;
let F be BinOp of D;
synonym F has_an_inverseOp for having_an_inverseOp F;
end;

definition
let D be non empty set ;
let F be BinOp of D;
assume that
A1: F has_a_unity and
A2: F is associative and
A3: F has_an_inverseOp ;
func the_inverseOp_wrt F -> UnOp of D means :Def3: :: FINSEQOP:def 3
it is_an_inverseOp_wrt F;
existence
ex b1 being UnOp of D st b1 is_an_inverseOp_wrt F
by A3, Def2;
uniqueness
for b1, b2 being UnOp of D st b1 is_an_inverseOp_wrt F & b2 is_an_inverseOp_wrt F holds
b1 = b2
proof end;
end;

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

theorem :: FINSEQOP:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSEQOP:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSEQOP:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th63: :: FINSEQOP:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for F being BinOp of D st F has_a_unity & F is associative & F has_an_inverseOp holds
( F . ((the_inverseOp_wrt F) . d),d = the_unity_wrt F & F . d,((the_inverseOp_wrt F) . d) = the_unity_wrt F )
proof end;

theorem Th64: :: FINSEQOP:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d1, d2 being Element of D
for F being BinOp of D st F has_a_unity & F is associative & F has_an_inverseOp & F . d1,d2 = the_unity_wrt F holds
( d1 = (the_inverseOp_wrt F) . d2 & (the_inverseOp_wrt F) . d1 = d2 )
proof end;

theorem Th65: :: FINSEQOP:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being BinOp of D st F has_a_unity & F is associative & F has_an_inverseOp holds
(the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F
proof end;

theorem Th66: :: FINSEQOP:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for F being BinOp of D st F has_a_unity & F is associative & F has_an_inverseOp holds
(the_inverseOp_wrt F) . ((the_inverseOp_wrt F) . d) = d
proof end;

theorem Th67: :: FINSEQOP:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being BinOp of D st F has_a_unity & F is associative & F is commutative & F has_an_inverseOp holds
the_inverseOp_wrt F is_distributive_wrt F
proof end;

theorem Th68: :: FINSEQOP:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d, d1, d2 being Element of D
for F being BinOp of D st F has_a_unity & F is associative & F has_an_inverseOp & ( F . d,d1 = F . d,d2 or F . d1,d = F . d2,d ) holds
d1 = d2
proof end;

theorem Th69: :: FINSEQOP:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d1, d2 being Element of D
for F being BinOp of D st F has_a_unity & F is associative & F has_an_inverseOp & ( F . d1,d2 = d2 or F . d2,d1 = d2 ) holds
d1 = the_unity_wrt F
proof end;

theorem Th70: :: FINSEQOP:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for e being Element of D
for F, G being BinOp of D st F is associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F & e = the_unity_wrt F holds
for d being Element of D holds
( G . e,d = e & G . d,e = e )
proof end;

theorem Th71: :: FINSEQOP:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 has_a_unity & F is associative & F has_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F holds
( u . (G . d1,d2) = G . (u . d1),d2 & u . (G . d1,d2) = G . d1,(u . d2) )
proof end;

theorem :: FINSEQOP:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F, G being BinOp of D
for u being UnOp of D st F has_a_unity & F is associative & F has_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F & G has_a_unity holds
G [;] (u . (the_unity_wrt G)),(id D) = u
proof end;

theorem :: FINSEQOP:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for F, G being BinOp of D st F is associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F holds
(G [;] d,(id D)) . (the_unity_wrt F) = the_unity_wrt F
proof end;

theorem :: FINSEQOP:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for F, G being BinOp of D st F is associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F holds
(G [:] (id D),d) . (the_unity_wrt F) = the_unity_wrt F
proof end;

theorem Th75: :: FINSEQOP:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, C being non empty set
for f being Function of C,D
for F being BinOp of D st F has_a_unity & F is associative & F has_an_inverseOp holds
( F .: f,((the_inverseOp_wrt F) * f) = C --> (the_unity_wrt F) & F .: ((the_inverseOp_wrt F) * f),f = C --> (the_unity_wrt F) )
proof end;

theorem Th76: :: FINSEQOP:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, C being non empty set
for f, f' being Function of C,D
for F being BinOp of D st F is associative & F has_an_inverseOp & F has_a_unity & F .: f,f' = C --> (the_unity_wrt F) holds
( f = (the_inverseOp_wrt F) * f' & (the_inverseOp_wrt F) * f = f' )
proof end;

theorem :: FINSEQOP:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for i being Nat
for T being Element of i -tuples_on D
for F being BinOp of D st F has_a_unity & F is associative & F has_an_inverseOp holds
( F .: T,((the_inverseOp_wrt F) * T) = i |-> (the_unity_wrt F) & F .: ((the_inverseOp_wrt F) * T),T = i |-> (the_unity_wrt F) )
proof end;

theorem :: FINSEQOP:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for i being Nat
for T1, T2 being Element of i -tuples_on D
for F being BinOp of D st F is associative & F has_an_inverseOp & F has_a_unity & F .: T1,T2 = i |-> (the_unity_wrt F) holds
( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 )
proof end;

theorem Th79: :: FINSEQOP:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 has_a_unity & e = the_unity_wrt F & F has_an_inverseOp & G is_distributive_wrt F holds
G [;] e,f = C --> e
proof end;

theorem :: FINSEQOP:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for e being Element of D
for i being Nat
for T being Element of i -tuples_on D
for F, G being BinOp of D st F is associative & F has_a_unity & e = the_unity_wrt F & F has_an_inverseOp & G is_distributive_wrt F holds
G [;] e,T = i |-> e
proof end;

definition
let F, f, g be Function;
func F * f,g -> Function equals :: FINSEQOP:def 4
F * [:f,g:];
correctness
coherence
F * [:f,g:] is Function
;
;
end;

:: deftheorem defines * FINSEQOP:def 4 :
for F, f, g being Function holds F * f,g = F * [:f,g:];

theorem :: FINSEQOP:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th82: :: FINSEQOP:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for F, f, g being Function st [x,y] in dom (F * f,g) holds
(F * f,g) . [x,y] = F . [(f . x),(g . y)]
proof end;

theorem Th83: :: FINSEQOP:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for F, f, g being Function st [x,y] in dom (F * f,g) holds
(F * f,g) . x,y = F . (f . x),(g . y) by Th82;

theorem Th84: :: FINSEQOP:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, D', E, C, C' being non empty set
for F being Function of [:D,D':],E
for f being Function of C,D
for g being Function of C',D' holds F * f,g is Function of [:C,C':],E
proof end;

theorem :: FINSEQOP:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being BinOp of D
for u, u' being Function of D,D holds F * u,u' is BinOp of D by Th84;

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

theorem Th86: :: FINSEQOP:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, D', E, C, C' being non empty set
for c being Element of C
for c' being Element of C'
for F being Function of [:D,D':],E
for f being Function of C,D
for g being Function of C',D' holds (F * f,g) . c,c' = F . (f . c),(g . c')
proof end;

theorem Th87: :: FINSEQOP:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d1, d2 being Element of D
for F being BinOp of D
for u being Function of D,D holds
( (F * (id D),u) . d1,d2 = F . d1,(u . d2) & (F * u,(id D)) . d1,d2 = F . (u . d1),d2 )
proof end;

theorem Th88: :: FINSEQOP:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D being non empty set
for f, f' being Function of C,D
for F being BinOp of D
for u being UnOp of D holds (F * (id D),u) .: f,f' = F .: f,(u * f')
proof end;

theorem :: FINSEQOP:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for i being Nat
for T1, T2 being Element of i -tuples_on D
for F being BinOp of D
for u being UnOp of D holds (F * (id D),u) .: T1,T2 = F .: T1,(u * T2)
proof end;

theorem :: FINSEQOP:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 has_a_unity & F is commutative & F has_an_inverseOp & u = the_inverseOp_wrt F holds
( u . ((F * (id D),u) . d1,d2) = (F * u,(id D)) . d1,d2 & (F * (id D),u) . d1,d2 = u . ((F * u,(id D)) . d1,d2) )
proof end;

theorem :: FINSEQOP:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for F being BinOp of D st F is associative & F has_a_unity & F has_an_inverseOp holds
(F * (id D),(the_inverseOp_wrt F)) . d,d = the_unity_wrt F
proof end;

theorem :: FINSEQOP:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for F being BinOp of D st F is associative & F has_a_unity & F has_an_inverseOp holds
(F * (id D),(the_inverseOp_wrt F)) . d,(the_unity_wrt F) = d
proof end;

theorem :: FINSEQOP:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for d being Element of D
for F being BinOp of D
for u being UnOp of D st F is associative & F has_a_unity & F has_an_inverseOp & u = the_inverseOp_wrt F holds
(F * (id D),u) . (the_unity_wrt F),d = u . d
proof end;

theorem :: FINSEQOP:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F, G being BinOp of D st F is commutative & F is associative & F has_a_unity & F has_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;