:: FINSEQOP semantic presentation

begin


theorem Th1: :: FINSEQOP:1
for f being Function holds
( <:{},f:> = {} & <:f,{}:> = {} )
proof
let f be Function; ::_thesis: ( <:{},f:> = {} & <:f,{}:> = {} )
 ( dom <:{},f:> = (dom {}) /\ (dom f) & dom <:f,{}:> = (dom f) /\ (dom {}) ) by FUNCT_3:def_7;
hence  ( <:{},f:> = {} & <:f,{}:> = {} ) ; ::_thesis: verum
end;

theorem :: FINSEQOP:2
for f being Function holds
( [:{},f:] = {} & [:f,{}:] = {} )
proof
let f be Function; ::_thesis: ( [:{},f:] = {} & [:f,{}:] = {} )
 ( dom [:{},f:] = [:(dom {}),(dom f):] & dom [:f,{}:] = [:(dom f),(dom {}):] ) by FUNCT_3:def_8;
hence  ( [:{},f:] = {} & [:f,{}:] = {} ) by ZFMISC_1:90; ::_thesis: verum
end;

theorem Th3: :: FINSEQOP:3
for F, f being Function holds
( F .: ({},f) = {} & F .: (f,{}) = {} )
proof
let F, f be Function; ::_thesis: ( F .: ({},f) = {} & F .: (f,{}) = {} )
 F .: ({},f) = F * {} by Th1;
hence  ( F .: ({},f) = {} & F .: (f,{}) = {} ) by Th1; ::_thesis: verum
end;

theorem :: FINSEQOP:4
for x being set
for F being Function holds F [:] ({},x) = {}
proof
let x be set ; ::_thesis: for F being Function holds F [:] ({},x) = {}
let F be Function; ::_thesis: F [:] ({},x) = {}
 F [:] ({},x) = F .: ({},((dom {}) --> x)) ;
hence  F [:] ({},x) = {} by Th3; ::_thesis: verum
end;

theorem :: FINSEQOP:5
for x being set
for F being Function holds F [;] (x,{}) = {}
proof
let x be set ; ::_thesis: for F being Function holds F [;] (x,{}) = {}
let F be Function; ::_thesis: F [;] (x,{}) = {}
 F [;] (x,{}) = F .: (((dom {}) --> x),{}) ;
hence  F [;] (x,{}) = {} by Th3; ::_thesis: verum
end;

theorem Th6: :: FINSEQOP:6
for X, x1, x2 being set holds <:(X --> x1),(X --> x2):> = X --> [x1,x2]
proof
let X be set ; ::_thesis: for x1, x2 being set holds <:(X --> x1),(X --> x2):> = X --> [x1,x2]
let x1, x2 be set ; ::_thesis: <:(X --> x1),(X --> x2):> = X --> [x1,x2]
set f = X --> x1;
set g = X --> x2;
set fg = <:(X --> x1),(X --> x2):>;
now__::_thesis:_<:(X_-->_x1),(X_-->_x2):>_=_X_-->_[x1,x2]
percases ( X = {} or X <> {} ) ;
supposeA1: X = {} ; ::_thesis: <:(X --> x1),(X --> x2):> = X --> [x1,x2]
thus  <:(X --> x1),(X --> x2):> = X --> [x1,x2] by A1; ::_thesis: verum
end;
supposeA2: X <> {} ; ::_thesis: <:(X --> x1),(X --> x2):> = X --> [x1,x2]
 rng <:(X --> x1),(X --> x2):> c= [:{x1},{x2}:] ;
then A3: rng <:(X --> x1),(X --> x2):> c= {[x1,x2]} by ZFMISC_1:29;
set x = the Element of X;
A4: ( dom (X --> x1) = X & dom (X --> x2) = X ) by FUNCOP_1:13;
then A5: dom <:(X --> x1),(X --> x2):> = X by FUNCT_3:50;
 ( (X --> x1) . the Element of X = x1 & (X --> x2) . the Element of X = x2 ) by A2, FUNCOP_1:7;
then  <:(X --> x1),(X --> x2):> . the Element of X = [x1,x2] by A2, A4, FUNCT_3:49;
then  [x1,x2] in rng <:(X --> x1),(X --> x2):> by A2, A5, FUNCT_1:def_3;
then  {[x1,x2]} c= rng <:(X --> x1),(X --> x2):> by ZFMISC_1:31;
then  rng <:(X --> x1),(X --> x2):> = {[x1,x2]} by A3, XBOOLE_0:def_10;
hence  <:(X --> x1),(X --> x2):> = X --> [x1,x2] by A5, FUNCOP_1:9; ::_thesis: verum
end;
end;
end;
hence  <:(X --> x1),(X --> x2):> = X --> [x1,x2] ; ::_thesis: verum
end;

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))
proof
let F be Function; ::_thesis: for X, x1, x2 being set st [x1,x2] in dom F holds
F .: ((X --> x1),(X --> x2)) = X --> (F . (x1,x2))
let X be set ; ::_thesis: for x1, x2 being set st [x1,x2] in dom F holds
F .: ((X --> x1),(X --> x2)) = X --> (F . (x1,x2))
let x1, x2 be set ; ::_thesis: ( [x1,x2] in dom F implies F .: ((X --> x1),(X --> x2)) = X --> (F . (x1,x2)) )
assume A1: [x1,x2] in dom F ; ::_thesis: F .: ((X --> x1),(X --> x2)) = X --> (F . (x1,x2))
set f = X --> x1;
set g = X --> x2;
thus F .: ((X --> x1),(X --> x2)) = F * (X --> [x1,x2]) by Th6
.= X --> (F . (x1,x2)) by A1, FUNCOP_1:17 ; ::_thesis: verum
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 funcF .: (p,p9) ->  FinSequence of E;
coherence
 F .: (p,p9) is FinSequence of E by FINSEQ_2:70;
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 d9 be Element of D9;
:: original: [:]
redefine funcF [:] (p,d9) ->  FinSequence of E;
coherence
 F [:] (p,d9) is FinSequence of E by FINSEQ_2:83;
end;

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 funcF [;] (d,p9) ->  FinSequence of E;
coherence
 F [;] (d,p9) is FinSequence of E by FINSEQ_2:77;
end;


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

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)*>
proof
let D, E be non empty set ; ::_thesis: 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)*>
let d be Element of D; ::_thesis: for p being FinSequence of D
for h being Function of D,E holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>
let p be FinSequence of D; ::_thesis: for h being Function of D,E holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>
let h be Function of D,E; ::_thesis: h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>
set q = h * (p ^ <*d*>);
set r = (h * p) ^ <*(h . d)*>;
set i = (len p) + 1;
A1: len (h * (p ^ <*d*>)) = len (p ^ <*d*>) by FINSEQ_2:33;
A2: len (h * p) = len p by FINSEQ_2:33;
 len (p ^ <*d*>) = (len p) + 1 by FINSEQ_2:16;
then A3: dom (h * (p ^ <*d*>)) = Seg ((len p) + 1) by A1, FINSEQ_1:def_3;
A4: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(h_*_(p_^_<*d*>))_holds_
(h_*_(p_^_<*d*>))_._j_=_((h_*_p)_^_<*(h_._d)*>)_._j
let j be Nat; ::_thesis: ( j in dom (h * (p ^ <*d*>)) implies (h * (p ^ <*d*>)) . j = ((h * p) ^ <*(h . d)*>) . j )
A5: Seg (len p) = dom p by FINSEQ_1:def_3;
A6: Seg (len (h * p)) = dom (h * p) by FINSEQ_1:def_3;
assume A7: j in dom (h * (p ^ <*d*>)) ; ::_thesis: (h * (p ^ <*d*>)) . j = ((h * p) ^ <*(h . d)*>) . j
now__::_thesis:_h_._((p_^_<*d*>)_._j)_=_((h_*_p)_^_<*(h_._d)*>)_._j
percases ( j in dom p or j = (len p) + 1 ) by A3, A7, A5, FINSEQ_2:7;
supposeA8: j in dom p ; ::_thesis: h . ((p ^ <*d*>) . j) = ((h * p) ^ <*(h . d)*>) . j
hence h . ((p ^ <*d*>) . j) = h . (p . j) by FINSEQ_1:def_7
.= (h * p) . j by A2, A5, A6, A8, FUNCT_1:12
.= ((h * p) ^ <*(h . d)*>) . j by A2, A5, A6, A8, FINSEQ_1:def_7 ;
::_thesis: verum
end;
supposeA9: j = (len p) + 1 ; ::_thesis: h . ((p ^ <*d*>) . j) = ((h * p) ^ <*(h . d)*>) . j
hence h . ((p ^ <*d*>) . j) = h . d by FINSEQ_1:42
.= ((h * p) ^ <*(h . d)*>) . j by A2, A9, FINSEQ_1:42 ;
::_thesis: verum
end;
end;
end;
hence  (h * (p ^ <*d*>)) . j = ((h * p) ^ <*(h . d)*>) . j by A7, FUNCT_1:12; ::_thesis: verum
end;
 len ((h * p) ^ <*(h . d)*>) = (len (h * p)) + 1 by FINSEQ_2:16;
hence  h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*> by A1, A2, A4, FINSEQ_2:9, FINSEQ_2:16; ::_thesis: verum
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)
proof
let D, E be non empty set ; ::_thesis: for p, q being FinSequence of D
for h being Function of D,E holds h * (p ^ q) = (h * p) ^ (h * q)
let p, q be FinSequence of D; ::_thesis: for h being Function of D,E holds h * (p ^ q) = (h * p) ^ (h * q)
let h be Function of D,E; ::_thesis: h * (p ^ q) = (h * p) ^ (h * q)
defpred S1[ FinSequence of D] means h * (p ^ $1) = (h * p) ^ (h * $1);
A1: for q being FinSequence of D
for d being Element of D st S1[q] holds
S1[q ^ <*d*>]
proof
let q be FinSequence of D; ::_thesis: for d being Element of D st S1[q] holds
S1[q ^ <*d*>]
let d be Element of D; ::_thesis: ( S1[q] implies S1[q ^ <*d*>] )
assume A2: h * (p ^ q) = (h * p) ^ (h * q) ; ::_thesis: S1[q ^ <*d*>]
thus h * (p ^ (q ^ <*d*>)) = h * ((p ^ q) ^ <*d*>) by FINSEQ_1:32
.= (h * (p ^ q)) ^ <*(h . d)*> by Th8
.= (h * p) ^ ((h * q) ^ <*(h . d)*>) by A2, FINSEQ_1:32
.= (h * p) ^ (h * (q ^ <*d*>)) by Th8 ; ::_thesis: verum
end;
h * (p ^ (<*> D)) = h * p by FINSEQ_1:34
.= (h * p) ^ (h * (<*> D)) by FINSEQ_1:34 ;
then A3: S1[ <*> D] ;
 for q being FinSequence of D holds S1[q] from FINSEQ_2:sch_2(A3, A1);
hence  h * (p ^ q) = (h * p) ^ (h * q) ; ::_thesis: verum
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
let D9, D, E be non empty set ; ::_thesis: 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
let i be Nat; ::_thesis: 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
let F be Function of [:D,D9:],E; ::_thesis: for T9 being Tuple of i,D9
for T being Tuple of 0 ,D holds F .: (T,T9) = <*> E
let T9 be Tuple of i,D9; ::_thesis: for T being Tuple of 0 ,D holds F .: (T,T9) = <*> E
let T be Tuple of 0 ,D; ::_thesis: F .: (T,T9) = <*> E
 T = <*> D ;
hence  F .: (T,T9) = <*> E by FINSEQ_2:73; ::_thesis: verum
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
let D, D9, E be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: for F being Function of [:D,D9:],E
for T9 being Tuple of 0 ,D9 holds F [;] (d,T9) = <*> E
let F be Function of [:D,D9:],E; ::_thesis: for T9 being Tuple of 0 ,D9 holds F [;] (d,T9) = <*> E
let T9 be Tuple of 0 ,D9; ::_thesis: F [;] (d,T9) = <*> E
 T9 = <*> D9 ;
hence  F [;] (d,T9) = <*> E by FINSEQ_2:79; ::_thesis: verum
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
let D9, D, E be non empty set ; ::_thesis: 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
let d9 be Element of D9; ::_thesis: for F being Function of [:D,D9:],E
for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E
let F be Function of [:D,D9:],E; ::_thesis: for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E
let T be Tuple of 0 ,D; ::_thesis: F [:] (T,d9) = <*> E
 T = <*> D ;
hence  F [:] (T,d9) = <*> E by FINSEQ_2:85; ::_thesis: verum
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))*>
proof
let E, D, D9 be non empty set ; ::_thesis: 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))*>
let d be Element of D; ::_thesis: 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))*>
let d9 be Element of D9; ::_thesis: 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))*>
let i be Nat; ::_thesis: 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))*>
let F be Function of [:D,D9:],E; ::_thesis: 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))*>
let T be Tuple of i,D; ::_thesis: for T9 being Tuple of i,D9 holds F .: ((T ^ <*d*>),(T9 ^ <*d9*>)) = (F .: (T,T9)) ^ <*(F . (d,d9))*>
let T9 be Tuple of i,D9; ::_thesis: F .: ((T ^ <*d*>),(T9 ^ <*d9*>)) = (F .: (T,T9)) ^ <*(F . (d,d9))*>
set p = T ^ <*d*>;
set q = T9 ^ <*d9*>;
set pq = F .: (T,T9);
set r = F .: ((T ^ <*d*>),(T9 ^ <*d9*>));
set s = (F .: (T,T9)) ^ <*(F . (d,d9))*>;
A1: len T9 = i by CARD_1:def_7;
then A2: len (T9 ^ <*d9*>) = i + 1 by FINSEQ_2:16;
A3: len T = i by CARD_1:def_7;
then A4: len (F .: (T,T9)) = i by A1, FINSEQ_2:72;
 len (T ^ <*d*>) = i + 1 by A3, FINSEQ_2:16;
then A5: len (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) = i + 1 by A2, FINSEQ_2:72;
then A6: dom (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) = Seg (i + 1) by FINSEQ_1:def_3;
A7: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(F_.:_((T_^_<*d*>),(T9_^_<*d9*>)))_holds_
(F_.:_((T_^_<*d*>),(T9_^_<*d9*>)))_._j_=_((F_.:_(T,T9))_^_<*(F_._(d,d9))*>)_._j
let j be Nat; ::_thesis: ( j in dom (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) implies (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) . j = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j )
assume A8: j in dom (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) ; ::_thesis: (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) . j = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j
now__::_thesis:_F_._(((T_^_<*d*>)_._j),((T9_^_<*d9*>)_._j))_=_((F_.:_(T,T9))_^_<*(F_._(d,d9))*>)_._j
percases ( j in Seg i or j = i + 1 ) by A6, A8, FINSEQ_2:7;
supposeA9: j in Seg i ; ::_thesis: F . (((T ^ <*d*>) . j),((T9 ^ <*d9*>) . j)) = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j
 Seg (len T) = dom T by FINSEQ_1:def_3;
then A10: (T ^ <*d*>) . j = T . j by A3, A9, FINSEQ_1:def_7;
A11: Seg (len (F .: (T,T9))) = dom (F .: (T,T9)) by FINSEQ_1:def_3;
 Seg (len T9) = dom T9 by FINSEQ_1:def_3;
then A12: (T9 ^ <*d9*>) . j = T9 . j by A1, A9, FINSEQ_1:def_7;
 j in dom (F .: (T,T9)) by A4, A9, FINSEQ_1:def_3;
hence F . (((T ^ <*d*>) . j),((T9 ^ <*d9*>) . j)) = (F .: (T,T9)) . j by A10, A12, FUNCOP_1:22
.= ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j by A4, A9, A11, FINSEQ_1:def_7 ;
::_thesis: verum
end;
supposeA13: j = i + 1 ; ::_thesis: F . (((T ^ <*d*>) . j),((T9 ^ <*d9*>) . j)) = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j
then  ( (T ^ <*d*>) . j = d & (T9 ^ <*d9*>) . j = d9 ) by A3, A1, FINSEQ_1:42;
hence  F . (((T ^ <*d*>) . j),((T9 ^ <*d9*>) . j)) = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j by A4, A13, FINSEQ_1:42; ::_thesis: verum
end;
end;
end;
hence  (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) . j = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j by A8, FUNCOP_1:22; ::_thesis: verum
end;
 len ((F .: (T,T9)) ^ <*(F . (d,d9))*>) = (len (F .: (T,T9))) + 1 by FINSEQ_2:16;
hence  F .: ((T ^ <*d*>),(T9 ^ <*d9*>)) = (F .: (T,T9)) ^ <*(F . (d,d9))*> by A5, A4, A7, FINSEQ_2:9; ::_thesis: verum
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))
proof
let E, D, D9 be non empty set ; ::_thesis: 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))
let i, j be Nat; ::_thesis: 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))
let F be Function of [:D,D9:],E; ::_thesis: 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))
let T be Tuple of i,D; ::_thesis: 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))
let T9 be Tuple of i,D9; ::_thesis: 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))
let S be Tuple of j,D; ::_thesis: for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
let S9 be Tuple of j,D9; ::_thesis: F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
defpred S1[ Nat] means  for S being Tuple of $1,D
for S9 being Tuple of $1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9));
now__::_thesis:_for_j_being_Nat_st_(_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))_)_holds_
for_S_being_Tuple_of_j_+_1,D
for_S9_being_Tuple_of_j_+_1,D9_holds_F_.:_((T_^_S),(T9_^_S9))_=_(F_.:_(T,T9))_^_(F_.:_(S,S9))
let j be Nat; ::_thesis: ( ( 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)) ) implies for S being Tuple of j + 1,D
for S9 being Tuple of j + 1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) )
assume A1: 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)) ; ::_thesis: for S being Tuple of j + 1,D
for S9 being Tuple of j + 1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
let S be Tuple of j + 1,D; ::_thesis: for S9 being Tuple of j + 1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
let S9 be Tuple of j + 1,D9; ::_thesis: F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
consider S1 being Element of j -tuples_on D, d being Element of D such that
A2: S = S1 ^ <*d*> by FINSEQ_2:117;
A3: T ^ S = (T ^ S1) ^ <*d*> by A2, FINSEQ_1:32;
reconsider S1 = S1 as Tuple of j,D ;
consider S19 being Element of j -tuples_on D9, d9 being Element of D9 such that
A4: S9 = S19 ^ <*d9*> by FINSEQ_2:117;
A5: T9 ^ S9 = (T9 ^ S19) ^ <*d9*> by A4, FINSEQ_1:32;
reconsider S19 = S19 as Tuple of j,D9 ;
 ( T ^ S1 is Tuple of i + j,D & T9 ^ S19 is Tuple of i + j,D9 ) by FINSEQ_2:107;
hence F .: ((T ^ S),(T9 ^ S9)) = (F .: ((T ^ S1),(T9 ^ S19))) ^ <*(F . (d,d9))*> by A3, A5, Th10
.= ((F .: (T,T9)) ^ (F .: (S1,S19))) ^ <*(F . (d,d9))*> by A1
.= (F .: (T,T9)) ^ ((F .: (S1,S19)) ^ <*(F . (d,d9))*>) by FINSEQ_1:32
.= (F .: (T,T9)) ^ (F .: (S,S9)) by A2, A4, Th10 ;
::_thesis: verum
end;
then A6: for j being Nat st S1[j] holds
S1[j + 1] ;
now__::_thesis:_for_S_being_Tuple_of_0_,D
for_S9_being_Tuple_of_0_,D9_holds_F_.:_((T_^_S),(T9_^_S9))_=_(F_.:_(T,T9))_^_(F_.:_(S,S9))
let S be Tuple of 0 ,D; ::_thesis: for S9 being Tuple of 0 ,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
let S9 be Tuple of 0 ,D9; ::_thesis: F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
 S = <*> D ;
then A7: F .: (S,S9) = <*> E by FINSEQ_2:73;
 ( T ^ S = T & T9 ^ S9 = T9 ) by FINSEQ_2:95;
hence  F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) by A7, FINSEQ_1:34; ::_thesis: verum
end;
then A8: S1[ 0 ] ;
 for j being Nat holds S1[j] from NAT_1:sch_2(A8, A6);
hence  F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) ; ::_thesis: verum
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))*>
proof
let D, E, D9 be non empty set ; ::_thesis: 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))*>
let d be Element of D; ::_thesis: 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))*>
let d9 be Element of D9; ::_thesis: 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))*>
let F be Function of [:D,D9:],E; ::_thesis: for p9 being FinSequence of D9 holds F [;] (d,(p9 ^ <*d9*>)) = (F [;] (d,p9)) ^ <*(F . (d,d9))*>
let p9 be FinSequence of D9; ::_thesis: F [;] (d,(p9 ^ <*d9*>)) = (F [;] (d,p9)) ^ <*(F . (d,d9))*>
set pd = p9 ^ <*d9*>;
set q = F [;] (d,p9);
set r = F [;] (d,(p9 ^ <*d9*>));
set s = (F [;] (d,p9)) ^ <*(F . (d,d9))*>;
set i = len p9;
A1: len (F [;] (d,p9)) = len p9 by FINSEQ_2:78;
 len (p9 ^ <*d9*>) = (len p9) + 1 by FINSEQ_2:16;
then A2: len (F [;] (d,(p9 ^ <*d9*>))) = (len p9) + 1 by FINSEQ_2:78;
then A3: dom (F [;] (d,(p9 ^ <*d9*>))) = Seg ((len p9) + 1) by FINSEQ_1:def_3;
A4: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(F_[;]_(d,(p9_^_<*d9*>)))_holds_
(F_[;]_(d,(p9_^_<*d9*>)))_._j_=_((F_[;]_(d,p9))_^_<*(F_._(d,d9))*>)_._j
let j be Nat; ::_thesis: ( j in dom (F [;] (d,(p9 ^ <*d9*>))) implies (F [;] (d,(p9 ^ <*d9*>))) . j = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j )
assume A5: j in dom (F [;] (d,(p9 ^ <*d9*>))) ; ::_thesis: (F [;] (d,(p9 ^ <*d9*>))) . j = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j
now__::_thesis:_F_._(d,((p9_^_<*d9*>)_._j))_=_((F_[;]_(d,p9))_^_<*(F_._(d,d9))*>)_._j
percases ( j in Seg (len p9) or j = (len p9) + 1 ) by A3, A5, FINSEQ_2:7;
supposeA6: j in Seg (len p9) ; ::_thesis: F . (d,((p9 ^ <*d9*>) . j)) = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j
then A7: j in dom (F [;] (d,p9)) by A1, FINSEQ_1:def_3;
A8: Seg (len (F [;] (d,p9))) = dom (F [;] (d,p9)) by FINSEQ_1:def_3;
 Seg (len p9) = dom p9 by FINSEQ_1:def_3;
hence F . (d,((p9 ^ <*d9*>) . j)) = F . (d,(p9 . j)) by A6, FINSEQ_1:def_7
.= (F [;] (d,p9)) . j by A7, FUNCOP_1:32
.= ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j by A1, A6, A8, FINSEQ_1:def_7 ;
::_thesis: verum
end;
supposeA9: j = (len p9) + 1 ; ::_thesis: F . (d,((p9 ^ <*d9*>) . j)) = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j
hence F . (d,((p9 ^ <*d9*>) . j)) = F . (d,d9) by FINSEQ_1:42
.= ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j by A1, A9, FINSEQ_1:42 ;
::_thesis: verum
end;
end;
end;
hence  (F [;] (d,(p9 ^ <*d9*>))) . j = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j by A5, FUNCOP_1:32; ::_thesis: verum
end;
 len ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) = (len (F [;] (d,p9))) + 1 by FINSEQ_2:16;
hence  F [;] (d,(p9 ^ <*d9*>)) = (F [;] (d,p9)) ^ <*(F . (d,d9))*> by A1, A2, A4, FINSEQ_2:9; ::_thesis: verum
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))
proof
let D, E, D9 be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let F be Function of [:D,D9:],E; ::_thesis: for p9, q9 being FinSequence of D9 holds F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9))
let p9, q9 be FinSequence of D9; ::_thesis: F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9))
defpred S1[ FinSequence of D9] means F [;] (d,(p9 ^ $1)) = (F [;] (d,p9)) ^ (F [;] (d,$1));
A1: for q9 being FinSequence of D9
for d9 being Element of D9 st S1[q9] holds
S1[q9 ^ <*d9*>]
proof
let q9 be FinSequence of D9; ::_thesis: for d9 being Element of D9 st S1[q9] holds
S1[q9 ^ <*d9*>]
let d9 be Element of D9; ::_thesis: ( S1[q9] implies S1[q9 ^ <*d9*>] )
assume A2: F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9)) ; ::_thesis: S1[q9 ^ <*d9*>]
thus F [;] (d,(p9 ^ (q9 ^ <*d9*>))) = F [;] (d,((p9 ^ q9) ^ <*d9*>)) by FINSEQ_1:32
.= (F [;] (d,(p9 ^ q9))) ^ <*(F . (d,d9))*> by Th12
.= (F [;] (d,p9)) ^ ((F [;] (d,q9)) ^ <*(F . (d,d9))*>) by A2, FINSEQ_1:32
.= (F [;] (d,p9)) ^ (F [;] (d,(q9 ^ <*d9*>))) by Th12 ; ::_thesis: verum
end;
F [;] (d,(p9 ^ (<*> D9))) = F [;] (d,p9) by FINSEQ_1:34
.= (F [;] (d,p9)) ^ (<*> E) by FINSEQ_1:34
.= (F [;] (d,p9)) ^ (F [;] (d,(<*> D9))) by FINSEQ_2:79 ;
then A3: S1[ <*> D9] ;
 for q9 being FinSequence of D9 holds S1[q9] from FINSEQ_2:sch_2(A3, A1);
hence  F [;] (d,(p9 ^ q9)) = (F [;] (d,p9)) ^ (F [;] (d,q9)) ; ::_thesis: verum
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))*>
proof
let D9, E, D be non empty set ; ::_thesis: 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))*>
let d be Element of D; ::_thesis: 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))*>
let d9 be Element of D9; ::_thesis: 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))*>
let F be Function of [:D,D9:],E; ::_thesis: for p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*>
let p be FinSequence of D; ::_thesis: F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*>
set pd = p ^ <*d*>;
set q = F [:] (p,d9);
set r = F [:] ((p ^ <*d*>),d9);
set s = (F [:] (p,d9)) ^ <*(F . (d,d9))*>;
set i = len p;
A1: len (F [:] (p,d9)) = len p by FINSEQ_2:84;
 len (p ^ <*d*>) = (len p) + 1 by FINSEQ_2:16;
then A2: len (F [:] ((p ^ <*d*>),d9)) = (len p) + 1 by FINSEQ_2:84;
then A3: dom (F [:] ((p ^ <*d*>),d9)) = Seg ((len p) + 1) by FINSEQ_1:def_3;
A4: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(F_[:]_((p_^_<*d*>),d9))_holds_
(F_[:]_((p_^_<*d*>),d9))_._j_=_((F_[:]_(p,d9))_^_<*(F_._(d,d9))*>)_._j
let j be Nat; ::_thesis: ( j in dom (F [:] ((p ^ <*d*>),d9)) implies (F [:] ((p ^ <*d*>),d9)) . j = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j )
assume A5: j in dom (F [:] ((p ^ <*d*>),d9)) ; ::_thesis: (F [:] ((p ^ <*d*>),d9)) . j = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j
now__::_thesis:_F_._(((p_^_<*d*>)_._j),d9)_=_((F_[:]_(p,d9))_^_<*(F_._(d,d9))*>)_._j
percases ( j in Seg (len p) or j = (len p) + 1 ) by A3, A5, FINSEQ_2:7;
supposeA6: j in Seg (len p) ; ::_thesis: F . (((p ^ <*d*>) . j),d9) = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j
then A7: j in dom (F [:] (p,d9)) by A1, FINSEQ_1:def_3;
 Seg (len p) = dom p by FINSEQ_1:def_3;
hence F . (((p ^ <*d*>) . j),d9) = F . ((p . j),d9) by A6, FINSEQ_1:def_7
.= (F [:] (p,d9)) . j by A7, FUNCOP_1:27
.= ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j by A7, FINSEQ_1:def_7 ;
::_thesis: verum
end;
supposeA8: j = (len p) + 1 ; ::_thesis: F . (((p ^ <*d*>) . j),d9) = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j
hence F . (((p ^ <*d*>) . j),d9) = F . (d,d9) by FINSEQ_1:42
.= ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j by A1, A8, FINSEQ_1:42 ;
::_thesis: verum
end;
end;
end;
hence  (F [:] ((p ^ <*d*>),d9)) . j = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j by A5, FUNCOP_1:27; ::_thesis: verum
end;
 len ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) = (len (F [:] (p,d9))) + 1 by FINSEQ_2:16;
hence  F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*> by A1, A2, A4, FINSEQ_2:9; ::_thesis: verum
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))
proof
let D9, E, D be non empty set ; ::_thesis: 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))
let d9 be Element of D9; ::_thesis: 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))
let F be Function of [:D,D9:],E; ::_thesis: for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))
let p, q be FinSequence of D; ::_thesis: F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))
defpred S1[ FinSequence of D] means F [:] ((p ^ $1),d9) = (F [:] (p,d9)) ^ (F [:] ($1,d9));
A1: for q being FinSequence of D
for d being Element of D st S1[q] holds
S1[q ^ <*d*>]
proof
let q be FinSequence of D; ::_thesis: for d being Element of D st S1[q] holds
S1[q ^ <*d*>]
let d be Element of D; ::_thesis: ( S1[q] implies S1[q ^ <*d*>] )
assume A2: F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) ; ::_thesis: S1[q ^ <*d*>]
thus F [:] ((p ^ (q ^ <*d*>)),d9) = F [:] (((p ^ q) ^ <*d*>),d9) by FINSEQ_1:32
.= (F [:] ((p ^ q),d9)) ^ <*(F . (d,d9))*> by Th14
.= (F [:] (p,d9)) ^ ((F [:] (q,d9)) ^ <*(F . (d,d9))*>) by A2, FINSEQ_1:32
.= (F [:] (p,d9)) ^ (F [:] ((q ^ <*d*>),d9)) by Th14 ; ::_thesis: verum
end;
F [:] ((p ^ (<*> D)),d9) = F [:] (p,d9) by FINSEQ_1:34
.= (F [:] (p,d9)) ^ (<*> E) by FINSEQ_1:34
.= (F [:] (p,d9)) ^ (F [:] ((<*> D),d9)) by FINSEQ_2:85 ;
then A3: S1[ <*> D] ;
 for q being FinSequence of D holds S1[q] from FINSEQ_2:sch_2(A3, A1);
hence  F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) ; ::_thesis: verum
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)
proof
let D, E be non empty set ; ::_thesis: for d being Element of D
for i being Nat
for h being Function of D,E holds h * (i |-> d) = i |-> (h . d)
let d be Element of D; ::_thesis: for i being Nat
for h being Function of D,E holds h * (i |-> d) = i |-> (h . d)
let i be Nat; ::_thesis: for h being Function of D,E holds h * (i |-> d) = i |-> (h . d)
let h be Function of D,E; ::_thesis: h * (i |-> d) = i |-> (h . d)
 d in D ;
then  d in dom h by FUNCT_2:def_1;
hence  h * (i |-> d) = i |-> (h . d) by FUNCOP_1:17; ::_thesis: verum
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))
proof
let D, D9, E be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let d9 be Element of D9; ::_thesis: for i being Nat
for F being Function of [:D,D9:],E holds F .: ((i |-> d),(i |-> d9)) = i |-> (F . (d,d9))
let i be Nat; ::_thesis: for F being Function of [:D,D9:],E holds F .: ((i |-> d),(i |-> d9)) = i |-> (F . (d,d9))
let F be Function of [:D,D9:],E; ::_thesis: F .: ((i |-> d),(i |-> d9)) = i |-> (F . (d,d9))
 [d,d9] in [:D,D9:] by ZFMISC_1:def_2;
then  [d,d9] in dom F by FUNCT_2:def_1;
hence  F .: ((i |-> d),(i |-> d9)) = i |-> (F . (d,d9)) by Th7; ::_thesis: verum
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))
proof
let D, D9, E be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let d9 be Element of D9; ::_thesis: for i being Nat
for F being Function of [:D,D9:],E holds F [;] (d,(i |-> d9)) = i |-> (F . (d,d9))
let i be Nat; ::_thesis: for F being Function of [:D,D9:],E holds F [;] (d,(i |-> d9)) = i |-> (F . (d,d9))
let F be Function of [:D,D9:],E; ::_thesis: F [;] (d,(i |-> d9)) = i |-> (F . (d,d9))
thus F [;] (d,(i |-> d9)) = F .: ((i |-> d),(i |-> d9)) by FUNCOP_1:13
.= i |-> (F . (d,d9)) by Th17 ; ::_thesis: verum
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))
proof
let D, D9, E be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let d9 be Element of D9; ::_thesis: for i being Nat
for F being Function of [:D,D9:],E holds F [:] ((i |-> d),d9) = i |-> (F . (d,d9))
let i be Nat; ::_thesis: for F being Function of [:D,D9:],E holds F [:] ((i |-> d),d9) = i |-> (F . (d,d9))
let F be Function of [:D,D9:],E; ::_thesis: F [:] ((i |-> d),d9) = i |-> (F . (d,d9))
thus F [:] ((i |-> d),d9) = F .: ((i |-> d),(i |-> d9)) by FUNCOP_1:13
.= i |-> (F . (d,d9)) by Th17 ; ::_thesis: verum
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)
proof
let D, E, D9 be non empty set ; ::_thesis: 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)
let d be Element of D; ::_thesis: 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)
let i be Nat; ::_thesis: for F being Function of [:D,D9:],E
for T9 being Tuple of i,D9 holds F .: ((i |-> d),T9) = F [;] (d,T9)
let F be Function of [:D,D9:],E; ::_thesis: for T9 being Tuple of i,D9 holds F .: ((i |-> d),T9) = F [;] (d,T9)
let T9 be Tuple of i,D9; ::_thesis: F .: ((i |-> d),T9) = F [;] (d,T9)
dom T9 = Seg (len T9) by FINSEQ_1:def_3
.= Seg i by CARD_1:def_7 ;
hence  F .: ((i |-> d),T9) = F [;] (d,T9) ; ::_thesis: verum
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)
proof
let D9, E, D be non empty set ; ::_thesis: 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)
let d be Element of D; ::_thesis: 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)
let i be Nat; ::_thesis: for F being Function of [:D,D9:],E
for T being Tuple of i,D holds F .: (T,(i |-> d)) = F [:] (T,d)
let F be Function of [:D,D9:],E; ::_thesis: for T being Tuple of i,D holds F .: (T,(i |-> d)) = F [:] (T,d)
let T be Tuple of i,D; ::_thesis: F .: (T,(i |-> d)) = F [:] (T,d)
dom T = Seg (len T) by FINSEQ_1:def_3
.= Seg i by CARD_1:def_7 ;
hence  F .: (T,(i |-> d)) = F [:] (T,d) ; ::_thesis: verum
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
proof
let D, E, D9 be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: 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
let i be Nat; ::_thesis: for F being Function of [:D,D9:],E
for T9 being Tuple of i,D9 holds F [;] (d,T9) = (F [;] (d,(id D9))) * T9
let F be Function of [:D,D9:],E; ::_thesis: for T9 being Tuple of i,D9 holds F [;] (d,T9) = (F [;] (d,(id D9))) * T9
let T9 be Tuple of i,D9; ::_thesis: F [;] (d,T9) = (F [;] (d,(id D9))) * T9
 rng T9 c= D9 ;
hence F [;] (d,T9) = F [;] (d,((id D9) * T9)) by RELAT_1:53
.= (F [;] (d,(id D9))) * T9 by FUNCOP_1:34 ;
::_thesis: verum
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
proof
let D9, E, D be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: 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
let i be Nat; ::_thesis: for F being Function of [:D,D9:],E
for T being Tuple of i,D holds F [:] (T,d) = (F [:] ((id D),d)) * T
let F be Function of [:D,D9:],E; ::_thesis: for T being Tuple of i,D holds F [:] (T,d) = (F [:] ((id D),d)) * T
let T be Tuple of i,D; ::_thesis: F [:] (T,d) = (F [:] ((id D),d)) * T
 rng T c= D ;
hence F [:] (T,d) = F [:] (((id D) * T),d) by RELAT_1:53
.= (F [:] ((id D),d)) * T by FUNCOP_1:29 ;
::_thesis: verum
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
let D be non empty set ; ::_thesis: for i being Nat
for T being Tuple of i,D holds T is Function of (Seg i),D
let i be Nat; ::_thesis: for T being Tuple of i,D holds T is Function of (Seg i),D
let T be Tuple of i,D; ::_thesis: T is Function of (Seg i),D
 len T = i by CARD_1:def_7;
then  Seg i = dom T by FINSEQ_1:def_3;
hence  T is Function of (Seg i),D by FINSEQ_2:26; ::_thesis: verum
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)
proof
let C, D be non empty set ; ::_thesis: 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)
let d be Element of D; ::_thesis: 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)
let f, f9 be Function of C,D; ::_thesis: 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)
let F be BinOp of D; ::_thesis: ( F is associative implies (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9) )
assume A1: F is associative ; ::_thesis: (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9)
now__::_thesis:_for_c_being_Element_of_C_holds_((F_[;]_(d,(id_D)))_*_(F_.:_(f,f9)))_._c_=_(F_.:_(((F_[;]_(d,(id_D)))_*_f),f9))_._c
let c be Element of C; ::_thesis: ((F [;] (d,(id D))) * (F .: (f,f9))) . c = (F .: (((F [;] (d,(id D))) * f),f9)) . c
thus ((F [;] (d,(id D))) * (F .: (f,f9))) . c = (F [;] (d,(id D))) . ((F .: (f,f9)) . c) by FUNCT_2:15
.= (F [;] (d,(id D))) . (F . ((f . c),(f9 . c))) by FUNCOP_1:37
.= F . (d,((id D) . (F . ((f . c),(f9 . c))))) by FUNCOP_1:53
.= F . (d,(F . ((f . c),(f9 . c)))) by FUNCT_1:18
.= F . ((F . (d,(f . c))),(f9 . c)) by A1, BINOP_1:def_3
.= F . (((F [;] (d,f)) . c),(f9 . c)) by FUNCOP_1:53
.= F . ((((F [;] (d,(id D))) * f) . c),(f9 . c)) by FUNCOP_1:55
.= (F .: (((F [;] (d,(id D))) * f),f9)) . c by FUNCOP_1:37 ; ::_thesis: verum
end;
hence  (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9) by FUNCT_2:63; ::_thesis: verum
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))
proof
let C, D be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let f, f9 be Function of C,D; ::_thesis: 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))
let F be BinOp of D; ::_thesis: ( F is associative implies (F [:] ((id D),d)) * (F .: (f,f9)) = F .: (f,((F [:] ((id D),d)) * f9)) )
assume A1: F is associative ; ::_thesis: (F [:] ((id D),d)) * (F .: (f,f9)) = F .: (f,((F [:] ((id D),d)) * f9))
now__::_thesis:_for_c_being_Element_of_C_holds_((F_[:]_((id_D),d))_*_(F_.:_(f,f9)))_._c_=_(F_.:_(f,((F_[:]_((id_D),d))_*_f9)))_._c
let c be Element of C; ::_thesis: ((F [:] ((id D),d)) * (F .: (f,f9))) . c = (F .: (f,((F [:] ((id D),d)) * f9))) . c
thus ((F [:] ((id D),d)) * (F .: (f,f9))) . c = (F [:] ((id D),d)) . ((F .: (f,f9)) . c) by FUNCT_2:15
.= (F [:] ((id D),d)) . (F . ((f . c),(f9 . c))) by FUNCOP_1:37
.= F . (((id D) . (F . ((f . c),(f9 . c)))),d) by FUNCOP_1:48
.= F . ((F . ((f . c),(f9 . c))),d) by FUNCT_1:18
.= F . ((f . c),(F . ((f9 . c),d))) by A1, BINOP_1:def_3
.= F . ((f . c),((F [:] (f9,d)) . c)) by FUNCOP_1:48
.= F . ((f . c),(((F [:] ((id D),d)) * f9) . c)) by FUNCOP_1:50
.= (F .: (f,((F [:] ((id D),d)) * f9))) . c by FUNCOP_1:37 ; ::_thesis: verum
end;
hence  (F [:] ((id D),d)) * (F .: (f,f9)) = F .: (f,((F [:] ((id D),d)) * f9)) by FUNCT_2:63; ::_thesis: verum
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)
proof
let D be non empty set ; ::_thesis: 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)
let d be Element of D; ::_thesis: 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)
let i be Nat; ::_thesis: 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)
let T1, T2 be Tuple of i,D; ::_thesis: 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)
let F be BinOp of D; ::_thesis: ( F is associative implies (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) )
assume A1: F is associative ; ::_thesis: (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2)
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2)
then  F .: (T1,T2) = <*> D by Lm1;
then A3: (F [;] (d,(id D))) * (F .: (T1,T2)) = <*> D ;
 T2 = <*> D by A2;
hence  (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) by A3, FINSEQ_2:73; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2)
then reconsider C = Seg i as non empty set ;
 ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4;
hence  (F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2) by A1, Th24; ::_thesis: verum
end;
end;
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))
proof
let D be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let i be Nat; ::_thesis: 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))
let T1, T2 be Tuple of i,D; ::_thesis: 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))
let F be BinOp of D; ::_thesis: ( F is associative implies (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) )
assume A1: F is associative ; ::_thesis: (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2))
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2))
then  F .: (T1,T2) = <*> D by Lm1;
then A3: (F [:] ((id D),d)) * (F .: (T1,T2)) = <*> D ;
 T1 = <*> D by A2;
hence  (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) by A3, FINSEQ_2:73; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2))
then reconsider C = Seg i as non empty set ;
 ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4;
hence  (F [:] ((id D),d)) * (F .: (T1,T2)) = F .: (T1,((F [:] ((id D),d)) * T2)) by A1, Th25; ::_thesis: verum
end;
end;
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)))
proof
let D be non empty set ; ::_thesis: 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)))
let i be Nat; ::_thesis: 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)))
let T1, T2, T3 be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative holds
F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3)))
let F be BinOp of D; ::_thesis: ( F is associative implies F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) )
assume A1: F is associative ; ::_thesis: F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3)))
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3)))
then  F .: (T1,T2) = <*> D by Lm1;
then A3: F .: ((F .: (T1,T2)),T3) = <*> D by FINSEQ_2:73;
 F .: (T2,T3) = <*> D by A2, Lm1;
hence  F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) by A3, FINSEQ_2:73; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3)))
then reconsider C = Seg i as non empty set ;
A4: T3 is Function of C,D by Lm4;
 ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4;
hence  F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) by A1, A4, FUNCOP_1:61; ::_thesis: verum
end;
end;
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)))
proof
let D be non empty set ; ::_thesis: 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)))
let d1, d2 be Element of D; ::_thesis: 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)))
let i be Nat; ::_thesis: 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)))
let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative holds
F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2)))
let F be BinOp of D; ::_thesis: ( F is associative implies F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) )
assume A1: F is associative ; ::_thesis: F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2)))
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2)))
then  F [;] (d1,T) = <*> D by Lm2;
then A3: F [:] ((F [;] (d1,T)),d2) = <*> D by FINSEQ_2:85;
 F [:] (T,d2) = <*> D by A2, Lm3;
hence  F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) by A3, FINSEQ_2:79; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2)))
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  F [:] ((F [;] (d1,T)),d2) = F [;] (d1,(F [:] (T,d2))) by A1, FUNCOP_1:59; ::_thesis: verum
end;
end;
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)))
proof
let D be non empty set ; ::_thesis: 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)))
let d be Element of D; ::_thesis: 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)))
let i be Nat; ::_thesis: 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)))
let T1, T2 be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative holds
F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2)))
let F be BinOp of D; ::_thesis: ( F is associative implies F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) )
assume A1: F is associative ; ::_thesis: F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2)))
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2)))
then  F [:] (T1,d) = <*> D by Lm3;
then A3: F .: ((F [:] (T1,d)),T2) = <*> D by FINSEQ_2:73;
 F [;] (d,T2) = <*> D by A2, Lm2;
hence  F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) by A3, FINSEQ_2:73; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2)))
then reconsider C = Seg i as non empty set ;
 ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4;
hence  F .: ((F [:] (T1,d)),T2) = F .: (T1,(F [;] (d,T2))) by A1, FUNCOP_1:60; ::_thesis: verum
end;
end;
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)))
proof
let D be non empty set ; ::_thesis: 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)))
let d1, d2 be Element of D; ::_thesis: 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)))
let i be Nat; ::_thesis: 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)))
let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative holds
F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T)))
let F be BinOp of D; ::_thesis: ( F is associative implies F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) )
assume A1: F is associative ; ::_thesis: F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T)))
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T)))
then  ( T = <*> D & F [;] (d2,T) = <*> D ) by Lm2;
hence  F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) ; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T)))
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T))) by A1, FUNCOP_1:62; ::_thesis: verum
end;
end;
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)
proof
let D be non empty set ; ::_thesis: 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)
let d1, d2 be Element of D; ::_thesis: 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)
let i be Nat; ::_thesis: 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)
let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is associative holds
F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)
let F be BinOp of D; ::_thesis: ( F is associative implies F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) )
assume A1: F is associative ; ::_thesis: F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)
then  ( T = <*> D & F [:] (T,d1) = <*> D ) by Lm3;
hence  F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) ; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) by A1, FUNCOP_1:63; ::_thesis: verum
end;
end;
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)
proof
let D be non empty set ; ::_thesis: 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)
let i be Nat; ::_thesis: 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)
let T1, T2 be Tuple of i,D; ::_thesis: for F being BinOp of D st F is commutative holds
F .: (T1,T2) = F .: (T2,T1)
let F be BinOp of D; ::_thesis: ( F is commutative implies F .: (T1,T2) = F .: (T2,T1) )
assume A1: F is commutative ; ::_thesis: F .: (T1,T2) = F .: (T2,T1)
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: F .: (T1,T2) = F .: (T2,T1)
then  F .: (T1,T2) = <*> D by Lm1;
hence  F .: (T1,T2) = F .: (T2,T1) by A2, Lm1; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: F .: (T1,T2) = F .: (T2,T1)
then reconsider C = Seg i as non empty set ;
 ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4;
hence  F .: (T1,T2) = F .: (T2,T1) by A1, FUNCOP_1:65; ::_thesis: verum
end;
end;
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)
proof
let D be non empty set ; ::_thesis: 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)
let d be Element of D; ::_thesis: 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)
let i be Nat; ::_thesis: for T being Tuple of i,D
for F being BinOp of D st F is commutative holds
F [;] (d,T) = F [:] (T,d)
let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is commutative holds
F [;] (d,T) = F [:] (T,d)
let F be BinOp of D; ::_thesis: ( F is commutative implies F [;] (d,T) = F [:] (T,d) )
assume A1: F is commutative ; ::_thesis: F [;] (d,T) = F [:] (T,d)
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: F [;] (d,T) = F [:] (T,d)
then  F [;] (d,T) = <*> D by Lm2;
hence  F [;] (d,T) = F [:] (T,d) by A2, Lm3; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: F [;] (d,T) = F [:] (T,d)
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  F [;] (d,T) = F [:] (T,d) by A1, FUNCOP_1:64; ::_thesis: verum
end;
end;
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)))
proof
let C, D be non empty set ; ::_thesis: 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)))
let d1, d2 be Element of D; ::_thesis: 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)))
let f be Function of C,D; ::_thesis: 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)))
let F, G be BinOp of D; ::_thesis: ( F is_distributive_wrt G implies F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f))) )
assume A1: F is_distributive_wrt G ; ::_thesis: F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f)))
now__::_thesis:_for_c_being_Element_of_C_holds_(F_[;]_((G_._(d1,d2)),f))_._c_=_(G_.:_((F_[;]_(d1,f)),(F_[;]_(d2,f))))_._c
let c be Element of C; ::_thesis: (F [;] ((G . (d1,d2)),f)) . c = (G .: ((F [;] (d1,f)),(F [;] (d2,f)))) . c
thus (F [;] ((G . (d1,d2)),f)) . c = F . ((G . (d1,d2)),(f . c)) by FUNCOP_1:53
.= G . ((F . (d1,(f . c))),(F . (d2,(f . c)))) by A1, BINOP_1:11
.= G . (((F [;] (d1,f)) . c),(F . (d2,(f . c)))) by FUNCOP_1:53
.= G . (((F [;] (d1,f)) . c),((F [;] (d2,f)) . c)) by FUNCOP_1:53
.= (G .: ((F [;] (d1,f)),(F [;] (d2,f)))) . c by FUNCOP_1:37 ; ::_thesis: verum
end;
hence  F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f))) by FUNCT_2:63; ::_thesis: verum
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)))
proof
let C, D be non empty set ; ::_thesis: 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)))
let d1, d2 be Element of D; ::_thesis: 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)))
let f be Function of C,D; ::_thesis: 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)))
let F, G be BinOp of D; ::_thesis: ( F is_distributive_wrt G implies F [:] (f,(G . (d1,d2))) = G .: ((F [:] (f,d1)),(F [:] (f,d2))) )
assume A1: F is_distributive_wrt G ; ::_thesis: F [:] (f,(G . (d1,d2))) = G .: ((F [:] (f,d1)),(F [:] (f,d2)))
now__::_thesis:_for_c_being_Element_of_C_holds_(F_[:]_(f,(G_._(d1,d2))))_._c_=_(G_.:_((F_[:]_(f,d1)),(F_[:]_(f,d2))))_._c
let c be Element of C; ::_thesis: (F [:] (f,(G . (d1,d2)))) . c = (G .: ((F [:] (f,d1)),(F [:] (f,d2)))) . c
thus (F [:] (f,(G . (d1,d2)))) . c = F . ((f . c),(G . (d1,d2))) by FUNCOP_1:48
.= G . ((F . ((f . c),d1)),(F . ((f . c),d2))) by A1, BINOP_1:11
.= G . (((F [:] (f,d1)) . c),(F . ((f . c),d2))) by FUNCOP_1:48
.= G . (((F [:] (f,d1)) . c),((F [:] (f,d2)) . c)) by FUNCOP_1:48
.= (G .: ((F [:] (f,d1)),(F [:] (f,d2)))) . c by FUNCOP_1:37 ; ::_thesis: verum
end;
hence  F [:] (f,(G . (d1,d2))) = G .: ((F [:] (f,d1)),(F [:] (f,d2))) by FUNCT_2:63; ::_thesis: verum
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))
proof
let C, E, D be non empty set ; ::_thesis: 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))
let f, f9 be Function of C,D; ::_thesis: 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))
let h be Function of D,E; ::_thesis: 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))
let F be BinOp of D; ::_thesis: 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))
let H be BinOp of E; ::_thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F .: (f,f9)) = H .: ((h * f),(h * f9)) )
assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h * (F .: (f,f9)) = H .: ((h * f),(h * f9))
now__::_thesis:_for_c_being_Element_of_C_holds_(h_*_(F_.:_(f,f9)))_._c_=_(H_.:_((h_*_f),(h_*_f9)))_._c
let c be Element of C; ::_thesis: (h * (F .: (f,f9))) . c = (H .: ((h * f),(h * f9))) . c
thus (h * (F .: (f,f9))) . c = h . ((F .: (f,f9)) . c) by FUNCT_2:15
.= h . (F . ((f . c),(f9 . c))) by FUNCOP_1:37
.= H . ((h . (f . c)),(h . (f9 . c))) by A1
.= H . (((h * f) . c),(h . (f9 . c))) by FUNCT_2:15
.= H . (((h * f) . c),((h * f9) . c)) by FUNCT_2:15
.= (H .: ((h * f),(h * f9))) . c by FUNCOP_1:37 ; ::_thesis: verum
end;
hence  h * (F .: (f,f9)) = H .: ((h * f),(h * f9)) by FUNCT_2:63; ::_thesis: verum
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))
proof
let C, E, D be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let f be Function of C,D; ::_thesis: 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))
let h be Function of D,E; ::_thesis: 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))
let F be BinOp of D; ::_thesis: 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))
let H be BinOp of E; ::_thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F [;] (d,f)) = H [;] ((h . d),(h * f)) )
assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h * (F [;] (d,f)) = H [;] ((h . d),(h * f))
reconsider g = C --> d as Function of C,D ;
A2: ( dom h = D & dom (h * f) = C ) by FUNCT_2:def_1;
thus h * (F [;] (d,f)) = h * (F .: (g,f)) by FUNCT_2:def_1
.= H .: ((h * g),(h * f)) by A1, Th37
.= H [;] ((h . d),(h * f)) by A2, FUNCOP_1:17 ; ::_thesis: verum
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))
proof
let C, E, D be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let f be Function of C,D; ::_thesis: 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))
let h be Function of D,E; ::_thesis: 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))
let F be BinOp of D; ::_thesis: 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))
let H be BinOp of E; ::_thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F [:] (f,d)) = H [:] ((h * f),(h . d)) )
assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h * (F [:] (f,d)) = H [:] ((h * f),(h . d))
reconsider g = C --> d as Function of C,D ;
A2: ( dom h = D & dom (h * f) = C ) by FUNCT_2:def_1;
thus h * (F [:] (f,d)) = h * (F .: (f,g)) by FUNCT_2:def_1
.= H .: ((h * f),(h * g)) by A1, Th37
.= H [:] ((h * f),(h . d)) by A2, FUNCOP_1:17 ; ::_thesis: verum
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))
proof
let C, D be non empty set ; ::_thesis: 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))
let f, f9 be Function of C,D; ::_thesis: 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))
let F be BinOp of D; ::_thesis: for u being UnOp of D st u is_distributive_wrt F holds
u * (F .: (f,f9)) = F .: ((u * f),(u * f9))
let u be UnOp of D; ::_thesis: ( u is_distributive_wrt F implies u * (F .: (f,f9)) = F .: ((u * f),(u * f9)) )
assume  for d1, d2 being Element of D holds u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) ; :: according to BINOP_1:def_20 ::_thesis: u * (F .: (f,f9)) = F .: ((u * f),(u * f9))
hence  u * (F .: (f,f9)) = F .: ((u * f),(u * f9)) by Th37; ::_thesis: verum
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))
proof
let C, D be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let f be Function of C,D; ::_thesis: 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))
let F be BinOp of D; ::_thesis: for u being UnOp of D st u is_distributive_wrt F holds
u * (F [;] (d,f)) = F [;] ((u . d),(u * f))
let u be UnOp of D; ::_thesis: ( u is_distributive_wrt F implies u * (F [;] (d,f)) = F [;] ((u . d),(u * f)) )
assume  for d1, d2 being Element of D holds u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) ; :: according to BINOP_1:def_20 ::_thesis: u * (F [;] (d,f)) = F [;] ((u . d),(u * f))
hence  u * (F [;] (d,f)) = F [;] ((u . d),(u * f)) by Th38; ::_thesis: verum
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))
proof
let C, D be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let f be Function of C,D; ::_thesis: 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))
let F be BinOp of D; ::_thesis: for u being UnOp of D st u is_distributive_wrt F holds
u * (F [:] (f,d)) = F [:] ((u * f),(u . d))
let u be UnOp of D; ::_thesis: ( u is_distributive_wrt F implies u * (F [:] (f,d)) = F [:] ((u * f),(u . d)) )
assume  for d1, d2 being Element of D holds u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) ; :: according to BINOP_1:def_20 ::_thesis: u * (F [:] (f,d)) = F [:] ((u * f),(u . d))
hence  u * (F [:] (f,d)) = F [:] ((u * f),(u . d)) by Th39; ::_thesis: verum
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 )
proof
let D, C be non empty set ; ::_thesis: 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 )
let f be Function of C,D; ::_thesis: 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 )
let F be BinOp of D; ::_thesis: ( F is having_a_unity implies ( F .: ((C --> (the_unity_wrt F)),f) = f & F .: (f,(C --> (the_unity_wrt F))) = f ) )
set e = the_unity_wrt F;
reconsider g = C --> (the_unity_wrt F) as Function of C,D ;
assume A1: F is having_a_unity ; ::_thesis: ( F .: ((C --> (the_unity_wrt F)),f) = f & F .: (f,(C --> (the_unity_wrt F))) = f )
now__::_thesis:_for_c_being_Element_of_C_holds_(F_.:_(g,f))_._c_=_f_._c
let c be Element of C; ::_thesis: (F .: (g,f)) . c = f . c
thus (F .: (g,f)) . c = F . ((g . c),(f . c)) by FUNCOP_1:37
.= F . ((the_unity_wrt F),(f . c)) by FUNCOP_1:7
.= f . c by A1, SETWISEO:15 ; ::_thesis: verum
end;
hence  F .: ((C --> (the_unity_wrt F)),f) = f by FUNCT_2:63; ::_thesis: F .: (f,(C --> (the_unity_wrt F))) = f
now__::_thesis:_for_c_being_Element_of_C_holds_(F_.:_(f,g))_._c_=_f_._c
let c be Element of C; ::_thesis: (F .: (f,g)) . c = f . c
thus (F .: (f,g)) . c = F . ((f . c),(g . c)) by FUNCOP_1:37
.= F . ((f . c),(the_unity_wrt F)) by FUNCOP_1:7
.= f . c by A1, SETWISEO:15 ; ::_thesis: verum
end;
hence  F .: (f,(C --> (the_unity_wrt F))) = f by FUNCT_2:63; ::_thesis: verum
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
proof
let C, D be non empty set ; ::_thesis: 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
let f be Function of C,D; ::_thesis: for F being BinOp of D st F is having_a_unity holds
F [;] ((the_unity_wrt F),f) = f
let F be BinOp of D; ::_thesis: ( F is having_a_unity implies F [;] ((the_unity_wrt F),f) = f )
set e = the_unity_wrt F;
assume A1: F is having_a_unity ; ::_thesis: F [;] ((the_unity_wrt F),f) = f
now__::_thesis:_for_c_being_Element_of_C_holds_(F_[;]_((the_unity_wrt_F),f))_._c_=_f_._c
let c be Element of C; ::_thesis: (F [;] ((the_unity_wrt F),f)) . c = f . c
thus (F [;] ((the_unity_wrt F),f)) . c = F . ((the_unity_wrt F),(f . c)) by FUNCOP_1:53
.= f . c by A1, SETWISEO:15 ; ::_thesis: verum
end;
hence  F [;] ((the_unity_wrt F),f) = f by FUNCT_2:63; ::_thesis: verum
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
proof
let C, D be non empty set ; ::_thesis: 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
let f be Function of C,D; ::_thesis: for F being BinOp of D st F is having_a_unity holds
F [:] (f,(the_unity_wrt F)) = f
let F be BinOp of D; ::_thesis: ( F is having_a_unity implies F [:] (f,(the_unity_wrt F)) = f )
set e = the_unity_wrt F;
assume A1: F is having_a_unity ; ::_thesis: F [:] (f,(the_unity_wrt F)) = f
now__::_thesis:_for_c_being_Element_of_C_holds_(F_[:]_(f,(the_unity_wrt_F)))_._c_=_f_._c
let c be Element of C; ::_thesis: (F [:] (f,(the_unity_wrt F))) . c = f . c
thus (F [:] (f,(the_unity_wrt F))) . c = F . ((f . c),(the_unity_wrt F)) by FUNCOP_1:48
.= f . c by A1, SETWISEO:15 ; ::_thesis: verum
end;
hence  F [:] (f,(the_unity_wrt F)) = f by FUNCT_2:63; ::_thesis: verum
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)))
proof
let D be non empty set ; ::_thesis: 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)))
let d1, d2 be Element of D; ::_thesis: 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)))
let i be Nat; ::_thesis: 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)))
let T be Tuple of i,D; ::_thesis: 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)))
let F, G be BinOp of D; ::_thesis: ( F is_distributive_wrt G implies F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) )
assume A1: F is_distributive_wrt G ; ::_thesis: F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T)))
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T)))
then  ( F [;] (d1,T) = <*> D & F [;] ((G . (d1,d2)),T) = <*> D ) by Lm2;
hence  F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) by FINSEQ_2:73; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T)))
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T))) by A1, Th35; ::_thesis: verum
end;
end;
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)))
proof
let D be non empty set ; ::_thesis: 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)))
let d1, d2 be Element of D; ::_thesis: 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)))
let i be Nat; ::_thesis: 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)))
let T be Tuple of i,D; ::_thesis: 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)))
let F, G be BinOp of D; ::_thesis: ( F is_distributive_wrt G implies F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) )
assume A1: F is_distributive_wrt G ; ::_thesis: F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2)))
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2)))
then  ( F [:] (T,d1) = <*> D & F [:] (T,(G . (d1,d2))) = <*> D ) by Lm3;
hence  F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) by FINSEQ_2:73; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2)))
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  F [:] (T,(G . (d1,d2))) = G .: ((F [:] (T,d1)),(F [:] (T,d2))) by A1, Th36; ::_thesis: verum
end;
end;
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))
proof
let E, D be non empty set ; ::_thesis: 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))
let i be Nat; ::_thesis: 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))
let h be Function of D,E; ::_thesis: 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))
let T1, T2 be Tuple of i,D; ::_thesis: 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))
let F be BinOp of D; ::_thesis: 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))
let H be BinOp of E; ::_thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) )
assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2))
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2))
then  F .: (T1,T2) = <*> D by Lm1;
then A3: h * (F .: (T1,T2)) = <*> E ;
 h * T1 = <*> E by A2;
hence  h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) by A3, FINSEQ_2:73; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2))
then reconsider C = Seg i as non empty set ;
 ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4;
hence  h * (F .: (T1,T2)) = H .: ((h * T1),(h * T2)) by A1, Th37; ::_thesis: verum
end;
end;
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))
proof
let E, D be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let i be Nat; ::_thesis: 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))
let h be Function of D,E; ::_thesis: 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))
let T be Tuple of i,D; ::_thesis: 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))
let F be BinOp of D; ::_thesis: 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))
let H be BinOp of E; ::_thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) )
assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h * (F [;] (d,T)) = H [;] ((h . d),(h * T))
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: h * (F [;] (d,T)) = H [;] ((h . d),(h * T))
then  F [;] (d,T) = <*> D by Lm2;
then A3: h * (F [;] (d,T)) = <*> E ;
 h * T = <*> E by A2;
hence  h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) by A3, FINSEQ_2:79; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: h * (F [;] (d,T)) = H [;] ((h . d),(h * T))
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  h * (F [;] (d,T)) = H [;] ((h . d),(h * T)) by A1, Th38; ::_thesis: verum
end;
end;
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))
proof
let E, D be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let i be Nat; ::_thesis: 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))
let h be Function of D,E; ::_thesis: 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))
let T be Tuple of i,D; ::_thesis: 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))
let F be BinOp of D; ::_thesis: 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))
let H be BinOp of E; ::_thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) )
assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h * (F [:] (T,d)) = H [:] ((h * T),(h . d))
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: h * (F [:] (T,d)) = H [:] ((h * T),(h . d))
then  F [:] (T,d) = <*> D by Lm3;
then A3: h * (F [:] (T,d)) = <*> E ;
 h * T = <*> E by A2;
hence  h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) by A3, FINSEQ_2:85; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: h * (F [:] (T,d)) = H [:] ((h * T),(h . d))
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  h * (F [:] (T,d)) = H [:] ((h * T),(h . d)) by A1, Th39; ::_thesis: verum
end;
end;
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))
proof
let D be non empty set ; ::_thesis: 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))
let i be Nat; ::_thesis: 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))
let T1, T2 be Tuple of i,D; ::_thesis: 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))
let F be BinOp of D; ::_thesis: for u being UnOp of D st u is_distributive_wrt F holds
u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2))
let u be UnOp of D; ::_thesis: ( u is_distributive_wrt F implies u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2)) )
assume  for d1, d2 being Element of D holds u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) ; :: according to BINOP_1:def_20 ::_thesis: u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2))
hence  u * (F .: (T1,T2)) = F .: ((u * T1),(u * T2)) by Th48; ::_thesis: verum
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))
proof
let D be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let i be Nat; ::_thesis: 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))
let T be Tuple of i,D; ::_thesis: 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))
let F be BinOp of D; ::_thesis: for u being UnOp of D st u is_distributive_wrt F holds
u * (F [;] (d,T)) = F [;] ((u . d),(u * T))
let u be UnOp of D; ::_thesis: ( u is_distributive_wrt F implies u * (F [;] (d,T)) = F [;] ((u . d),(u * T)) )
assume  for d1, d2 being Element of D holds u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) ; :: according to BINOP_1:def_20 ::_thesis: u * (F [;] (d,T)) = F [;] ((u . d),(u * T))
hence  u * (F [;] (d,T)) = F [;] ((u . d),(u * T)) by Th49; ::_thesis: verum
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))
proof
let D be non empty set ; ::_thesis: 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))
let d be Element of D; ::_thesis: 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))
let i be Nat; ::_thesis: 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))
let T be Tuple of i,D; ::_thesis: 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))
let F be BinOp of D; ::_thesis: for u being UnOp of D st u is_distributive_wrt F holds
u * (F [:] (T,d)) = F [:] ((u * T),(u . d))
let u be UnOp of D; ::_thesis: ( u is_distributive_wrt F implies u * (F [:] (T,d)) = F [:] ((u * T),(u . d)) )
assume  for d1, d2 being Element of D holds u . (F . (d1,d2)) = F . ((u . d1),(u . d2)) ; :: according to BINOP_1:def_20 ::_thesis: u * (F [:] (T,d)) = F [:] ((u * T),(u . d))
hence  u * (F [:] (T,d)) = F [:] ((u * T),(u . d)) by Th50; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: 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
let G, F be BinOp of D; ::_thesis: for u being UnOp of D st G is_distributive_wrt F & u = G [;] (d,(id D)) holds
u is_distributive_wrt F
let u be UnOp of D; ::_thesis: ( G is_distributive_wrt F & u = G [;] (d,(id D)) implies u is_distributive_wrt F )
assume that
A1: G is_distributive_wrt F and
A2: u = G [;] (d,(id D)) ; ::_thesis: u is_distributive_wrt F
let d1 be Element of D; :: according to BINOP_1:def_20 ::_thesis: for b1 being Element of D holds u . (F . (d1,b1)) = F . ((u . d1),(u . b1))
let d2 be Element of D; ::_thesis: u . (F . (d1,d2)) = F . ((u . d1),(u . d2))
thus u . (F . (d1,d2)) = G . (d,((id D) . (F . (d1,d2)))) by A2, FUNCOP_1:53
.= G . (d,(F . (d1,d2))) by FUNCT_1:18
.= F . ((G . (d,d1)),(G . (d,d2))) by A1, BINOP_1:11
.= F . ((G . (d,((id D) . d1))),(G . (d,d2))) by FUNCT_1:18
.= F . ((G . (d,((id D) . d1))),(G . (d,((id D) . d2)))) by FUNCT_1:18
.= F . ((u . d1),(G . (d,((id D) . d2)))) by A2, FUNCOP_1:53
.= F . ((u . d1),(u . d2)) by A2, FUNCOP_1:53 ; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: 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
let G, F be BinOp of D; ::_thesis: for u being UnOp of D st G is_distributive_wrt F & u = G [:] ((id D),d) holds
u is_distributive_wrt F
let u be UnOp of D; ::_thesis: ( G is_distributive_wrt F & u = G [:] ((id D),d) implies u is_distributive_wrt F )
assume that
A1: G is_distributive_wrt F and
A2: u = G [:] ((id D),d) ; ::_thesis: u is_distributive_wrt F
let d1 be Element of D; :: according to BINOP_1:def_20 ::_thesis: for b1 being Element of D holds u . (F . (d1,b1)) = F . ((u . d1),(u . b1))
let d2 be Element of D; ::_thesis: u . (F . (d1,d2)) = F . ((u . d1),(u . d2))
thus u . (F . (d1,d2)) = G . (((id D) . (F . (d1,d2))),d) by A2, FUNCOP_1:48
.= G . ((F . (d1,d2)),d) by FUNCT_1:18
.= F . ((G . (d1,d)),(G . (d2,d))) by A1, BINOP_1:11
.= F . ((G . (((id D) . d1),d)),(G . (d2,d))) by FUNCT_1:18
.= F . ((G . (((id D) . d1),d)),(G . (((id D) . d2),d))) by FUNCT_1:18
.= F . ((u . d1),(G . (((id D) . d2),d))) by A2, FUNCOP_1:48
.= F . ((u . d1),(u . d2)) by A2, FUNCOP_1:48 ; ::_thesis: verum
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 )
proof
let D be non empty set ; ::_thesis: 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 )
let i be Nat; ::_thesis: 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 )
let T be Tuple of i,D; ::_thesis: 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 )
let F be BinOp of D; ::_thesis: ( F is having_a_unity implies ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) )
assume A1: F is having_a_unity ; ::_thesis: ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T )
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T )
then  T = <*> D ;
hence  ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) by A2, Lm1; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T )
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  ( F .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T ) by A1, Th43; ::_thesis: verum
end;
end;
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
proof
let D be non empty set ; ::_thesis: 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
let i be Nat; ::_thesis: 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
let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is having_a_unity holds
F [;] ((the_unity_wrt F),T) = T
let F be BinOp of D; ::_thesis: ( F is having_a_unity implies F [;] ((the_unity_wrt F),T) = T )
assume A1: F is having_a_unity ; ::_thesis: F [;] ((the_unity_wrt F),T) = T
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: F [;] ((the_unity_wrt F),T) = T
then  T = <*> D ;
hence  F [;] ((the_unity_wrt F),T) = T by Lm2; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: F [;] ((the_unity_wrt F),T) = T
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  F [;] ((the_unity_wrt F),T) = T by A1, Th44; ::_thesis: verum
end;
end;
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
proof
let D be non empty set ; ::_thesis: 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
let i be Nat; ::_thesis: 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
let T be Tuple of i,D; ::_thesis: for F being BinOp of D st F is having_a_unity holds
F [:] (T,(the_unity_wrt F)) = T
let F be BinOp of D; ::_thesis: ( F is having_a_unity implies F [:] (T,(the_unity_wrt F)) = T )
assume A1: F is having_a_unity ; ::_thesis: F [:] (T,(the_unity_wrt F)) = T
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: F [:] (T,(the_unity_wrt F)) = T
then  T = <*> D ;
hence  F [:] (T,(the_unity_wrt F)) = T by Lm3; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: F [:] (T,(the_unity_wrt F)) = T
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  F [:] (T,(the_unity_wrt F)) = T by A1, Th45; ::_thesis: verum
end;
end;
end;

definition
let D be non empty set ;
let u be UnOp of D;
let F be BinOp of D;
predu 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;
attrF 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 );

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 ;
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
set e = the_unity_wrt F;
let u1, u2 be UnOp of D; ::_thesis: ( u1 is_an_inverseOp_wrt F & u2 is_an_inverseOp_wrt F implies u1 = u2 )
assume that
A4: for d being Element of D holds
( F . (d,(u1 . d)) = the_unity_wrt F & F . ((u1 . d),d) = the_unity_wrt F ) and
A5: for d being Element of D holds
( F . (d,(u2 . d)) = the_unity_wrt F & F . ((u2 . d),d) = the_unity_wrt F ) ; :: according to FINSEQOP:def_1 ::_thesis: u1 = u2
now__::_thesis:_for_d_being_Element_of_D_holds_u1_._d_=_u2_._d
let d be Element of D; ::_thesis: u1 . d = u2 . d
set d1 = u1 . d;
set d2 = u2 . d;
thus u1 . d = F . ((u1 . d),(the_unity_wrt F)) by A1, SETWISEO:15
.= F . ((u1 . d),(F . (d,(u2 . d)))) by A5
.= F . ((F . ((u1 . d),d)),(u2 . d)) by A2, BINOP_1:def_3
.= F . ((the_unity_wrt F),(u2 . d)) by A4
.= u2 . d by A1, SETWISEO:15 ; ::_thesis: verum
end;
hence  u1 = u2 by FUNCT_2:63; ::_thesis: verum
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 is having_a_unity & F is associative & F is having_an_inverseOp holds
for b3 being UnOp of D holds
( b3 = the_inverseOp_wrt F iff b3 is_an_inverseOp_wrt F );

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 )
proof
let D be non empty set ; ::_thesis: 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 )
let d be Element of D; ::_thesis: 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 )
let F be BinOp of D; ::_thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp implies ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F ) )
assume  ( F is having_a_unity & F is associative & F is having_an_inverseOp ) ; ::_thesis: ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F )
then  the_inverseOp_wrt F is_an_inverseOp_wrt F by Def3;
hence  ( F . (((the_inverseOp_wrt F) . d),d) = the_unity_wrt F & F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F ) by Def1; ::_thesis: verum
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 )
proof
let D be non empty set ; ::_thesis: 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 )
let d1, d2 be Element of D; ::_thesis: 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 )
let F be BinOp of D; ::_thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp & F . (d1,d2) = the_unity_wrt F implies ( d1 = (the_inverseOp_wrt F) . d2 & (the_inverseOp_wrt F) . d1 = d2 ) )
assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is having_an_inverseOp and
A4: F . (d1,d2) = the_unity_wrt F ; ::_thesis: ( d1 = (the_inverseOp_wrt F) . d2 & (the_inverseOp_wrt F) . d1 = d2 )
set e = the_unity_wrt F;
set d3 = (the_inverseOp_wrt F) . d2;
 F . ((F . (d1,d2)),((the_inverseOp_wrt F) . d2)) = (the_inverseOp_wrt F) . d2 by A1, A4, SETWISEO:15;
then  F . (d1,(F . (d2,((the_inverseOp_wrt F) . d2)))) = (the_inverseOp_wrt F) . d2 by A2, BINOP_1:def_3;
then  F . (d1,(the_unity_wrt F)) = (the_inverseOp_wrt F) . d2 by A1, A2, A3, Th59;
hence  d1 = (the_inverseOp_wrt F) . d2 by A1, SETWISEO:15; ::_thesis: (the_inverseOp_wrt F) . d1 = d2
set d3 = (the_inverseOp_wrt F) . d1;
 F . (((the_inverseOp_wrt F) . d1),(F . (d1,d2))) = (the_inverseOp_wrt F) . d1 by A1, A4, SETWISEO:15;
then  F . ((F . (((the_inverseOp_wrt F) . d1),d1)),d2) = (the_inverseOp_wrt F) . d1 by A2, BINOP_1:def_3;
then  F . ((the_unity_wrt F),d2) = (the_inverseOp_wrt F) . d1 by A1, A2, A3, Th59;
hence  (the_inverseOp_wrt F) . d1 = d2 by A1, SETWISEO:15; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let F be BinOp of D; ::_thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp implies (the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F )
assume that
A1: F is having_a_unity and
A2: ( F is associative & F is having_an_inverseOp ) ; ::_thesis: (the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F
set e = the_unity_wrt F;
 F . ((the_unity_wrt F),(the_unity_wrt F)) = the_unity_wrt F by A1, SETWISEO:15;
hence  (the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F by A1, A2, Th60; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: 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
let F be BinOp of D; ::_thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp implies (the_inverseOp_wrt F) . ((the_inverseOp_wrt F) . d) = d )
assume A1: ( F is having_a_unity & F is associative & F is having_an_inverseOp ) ; ::_thesis: (the_inverseOp_wrt F) . ((the_inverseOp_wrt F) . d) = d
then  F . (d,((the_inverseOp_wrt F) . d)) = the_unity_wrt F by Th59;
hence  (the_inverseOp_wrt F) . ((the_inverseOp_wrt F) . d) = d by A1, Th60; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let F be BinOp of D; ::_thesis: ( F is having_a_unity & F is associative & F is commutative & F is having_an_inverseOp implies the_inverseOp_wrt F is_distributive_wrt F )
assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is commutative and
A4: F is having_an_inverseOp ; ::_thesis: the_inverseOp_wrt F is_distributive_wrt F
let d1 be Element of D; :: according to BINOP_1:def_20 ::_thesis: for b1 being Element of D holds (the_inverseOp_wrt F) . (F . (d1,b1)) = F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . b1))
let d2 be Element of D; ::_thesis: (the_inverseOp_wrt F) . (F . (d1,d2)) = F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . d2))
set e = the_unity_wrt F;
set u = the_inverseOp_wrt F;
F . ((F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . d2))),(F . (d1,d2))) = F . (((the_inverseOp_wrt F) . d1),(F . (((the_inverseOp_wrt F) . d2),(F . (d1,d2))))) by A2, BINOP_1:def_3
.= F . (((the_inverseOp_wrt F) . d1),(F . ((F . (((the_inverseOp_wrt F) . d2),d1)),d2))) by A2, BINOP_1:def_3
.= F . (((the_inverseOp_wrt F) . d1),(F . ((F . (d1,((the_inverseOp_wrt F) . d2))),d2))) by A3, BINOP_1:def_2
.= F . (((the_inverseOp_wrt F) . d1),(F . (d1,(F . (((the_inverseOp_wrt F) . d2),d2))))) by A2, BINOP_1:def_3
.= F . (((the_inverseOp_wrt F) . d1),(F . (d1,(the_unity_wrt F)))) by A1, A2, A4, Th59
.= F . ((F . (((the_inverseOp_wrt F) . d1),d1)),(the_unity_wrt F)) by A2, BINOP_1:def_3
.= F . ((the_unity_wrt F),(the_unity_wrt F)) by A1, A2, A4, Th59
.= the_unity_wrt F by A1, SETWISEO:15 ;
hence  (the_inverseOp_wrt F) . (F . (d1,d2)) = F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . d2)) by A1, A2, A4, Th60; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let d, d1, d2 be Element of D; ::_thesis: 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
let F be BinOp of D; ::_thesis: ( 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) ) implies d1 = d2 )
assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is having_an_inverseOp and
A4: ( F . (d,d1) = F . (d,d2) or F . (d1,d) = F . (d2,d) ) ; ::_thesis: d1 = d2
set e = the_unity_wrt F;
set u = the_inverseOp_wrt F;
percases ( F . (d,d1) = F . (d,d2) or F . (d1,d) = F . (d2,d) ) by A4;
supposeA5: F . (d,d1) = F . (d,d2) ; ::_thesis: d1 = d2
thus d1 = F . ((the_unity_wrt F),d1) by A1, SETWISEO:15
.= F . ((F . (((the_inverseOp_wrt F) . d),d)),d1) by A1, A2, A3, Th59
.= F . (((the_inverseOp_wrt F) . d),(F . (d,d2))) by A2, A5, BINOP_1:def_3
.= F . ((F . (((the_inverseOp_wrt F) . d),d)),d2) by A2, BINOP_1:def_3
.= F . ((the_unity_wrt F),d2) by A1, A2, A3, Th59
.= d2 by A1, SETWISEO:15 ; ::_thesis: verum
end;
supposeA6: F . (d1,d) = F . (d2,d) ; ::_thesis: d1 = d2
thus d1 = F . (d1,(the_unity_wrt F)) by A1, SETWISEO:15
.= F . (d1,(F . (d,((the_inverseOp_wrt F) . d)))) by A1, A2, A3, Th59
.= F . ((F . (d2,d)),((the_inverseOp_wrt F) . d)) by A2, A6, BINOP_1:def_3
.= F . (d2,(F . (d,((the_inverseOp_wrt F) . d)))) by A2, BINOP_1:def_3
.= F . (d2,(the_unity_wrt F)) by A1, A2, A3, Th59
.= d2 by A1, SETWISEO:15 ; ::_thesis: verum
end;
end;
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
proof
let D be non empty set ; ::_thesis: 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
let d1, d2 be Element of D; ::_thesis: 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
let F be BinOp of D; ::_thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp & ( F . (d1,d2) = d2 or F . (d2,d1) = d2 ) implies d1 = the_unity_wrt F )
assume that
A1: F is having_a_unity and
A2: ( F is associative & F is having_an_inverseOp ) ; ::_thesis: ( ( not F . (d1,d2) = d2 & not F . (d2,d1) = d2 ) or d1 = the_unity_wrt F )
set e = the_unity_wrt F;
assume  ( F . (d1,d2) = d2 or F . (d2,d1) = d2 ) ; ::_thesis: d1 = the_unity_wrt F
then  ( F . (d1,d2) = F . ((the_unity_wrt F),d2) or F . (d2,d1) = F . (d2,(the_unity_wrt F)) ) by A1, SETWISEO:15;
hence  d1 = the_unity_wrt F by A1, A2, Th64; ::_thesis: verum
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 )
proof
let D be non empty set ; ::_thesis: 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 )
let e be Element of D; ::_thesis: 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 )
let F, G be BinOp of D; ::_thesis: ( F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F & e = the_unity_wrt F implies for d being Element of D holds
( G . (e,d) = e & G . (d,e) = e ) )
assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp and
A4: G is_distributive_wrt F and
A5: e = the_unity_wrt F ; ::_thesis: for d being Element of D holds
( G . (e,d) = e & G . (d,e) = e )
let d be Element of D; ::_thesis: ( G . (e,d) = e & G . (d,e) = e )
set ed = G . (e,d);
F . ((G . (e,d)),(G . (e,d))) = G . ((F . (e,e)),d) by A4, BINOP_1:11
.= G . (e,d) by A2, A5, SETWISEO:15 ;
hence  G . (e,d) = e by A1, A2, A3, A5, Th65; ::_thesis: G . (d,e) = e
set de = G . (d,e);
F . ((G . (d,e)),(G . (d,e))) = G . (d,(F . (e,e))) by A4, BINOP_1:11
.= G . (d,e) by A2, A5, SETWISEO:15 ;
hence  G . (d,e) = e by A1, A2, A3, A5, Th65; ::_thesis: verum
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)) )
proof
let D be non empty set ; ::_thesis: 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)) )
let d1, d2 be Element of D; ::_thesis: 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)) )
let F, G be BinOp of D; ::_thesis: 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)) )
let u be UnOp of D; ::_thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F implies ( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) ) )
assume that
A1: ( F is having_a_unity & F is associative & F is having_an_inverseOp ) and
A2: u = the_inverseOp_wrt F and
A3: G is_distributive_wrt F ; ::_thesis: ( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) )
set e = the_unity_wrt F;
F . ((G . (d1,d2)),(G . ((u . d1),d2))) = G . ((F . (d1,(u . d1))),d2) by A3, BINOP_1:11
.= G . ((the_unity_wrt F),d2) by A1, A2, Th59
.= the_unity_wrt F by A1, A3, Th66 ;
hence  u . (G . (d1,d2)) = G . ((u . d1),d2) by A1, A2, Th60; ::_thesis: u . (G . (d1,d2)) = G . (d1,(u . d2))
F . ((G . (d1,d2)),(G . (d1,(u . d2)))) = G . (d1,(F . (d2,(u . d2)))) by A3, BINOP_1:11
.= G . (d1,(the_unity_wrt F)) by A1, A2, Th59
.= the_unity_wrt F by A1, A3, Th66 ;
hence  u . (G . (d1,d2)) = G . (d1,(u . d2)) by A1, A2, Th60; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let F, G be BinOp of D; ::_thesis: 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
let u be UnOp of D; ::_thesis: ( 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 implies G [;] ((u . (the_unity_wrt G)),(id D)) = u )
assume that
A1: ( F is having_a_unity & F is associative & F is having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F ) and
A2: G is having_a_unity ; ::_thesis: G [;] ((u . (the_unity_wrt G)),(id D)) = u
set o = the_unity_wrt G;
 for d being Element of D holds (G [;] ((u . (the_unity_wrt G)),(id D))) . d = u . d
proof
let d be Element of D; ::_thesis: (G [;] ((u . (the_unity_wrt G)),(id D))) . d = u . d
thus (G [;] ((u . (the_unity_wrt G)),(id D))) . d = G . ((u . (the_unity_wrt G)),((id D) . d)) by FUNCOP_1:53
.= G . ((u . (the_unity_wrt G)),d) by FUNCT_1:18
.= u . (G . ((the_unity_wrt G),d)) by A1, Th67
.= u . d by A2, SETWISEO:15 ; ::_thesis: verum
end;
hence  G [;] ((u . (the_unity_wrt G)),(id D)) = u by FUNCT_2:63; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: 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
let F, G be BinOp of D; ::_thesis: ( F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies (G [;] (d,(id D))) . (the_unity_wrt F) = the_unity_wrt F )
assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp and
A4: G is_distributive_wrt F ; ::_thesis: (G [;] (d,(id D))) . (the_unity_wrt F) = the_unity_wrt F
set e = the_unity_wrt F;
set i = the_inverseOp_wrt F;
G . (d,(the_unity_wrt F)) = G . (d,(F . ((the_unity_wrt F),(the_unity_wrt F)))) by A2, SETWISEO:15
.= F . ((G . (d,(the_unity_wrt F))),(G . (d,(the_unity_wrt F)))) by A4, BINOP_1:11 ;
then  the_unity_wrt F = F . ((F . ((G . (d,(the_unity_wrt F))),(G . (d,(the_unity_wrt F))))),((the_inverseOp_wrt F) . (G . (d,(the_unity_wrt F))))) by A1, A2, A3, Th59;
then  the_unity_wrt F = F . ((G . (d,(the_unity_wrt F))),(F . ((G . (d,(the_unity_wrt F))),((the_inverseOp_wrt F) . (G . (d,(the_unity_wrt F))))))) by A1, BINOP_1:def_3;
then  the_unity_wrt F = F . ((G . (d,(the_unity_wrt F))),(the_unity_wrt F)) by A1, A2, A3, Th59;
then  the_unity_wrt F = G . (d,(the_unity_wrt F)) by A2, SETWISEO:15;
then  G . (d,((id D) . (the_unity_wrt F))) = the_unity_wrt F by FUNCT_1:18;
hence  (G [;] (d,(id D))) . (the_unity_wrt F) = the_unity_wrt F by FUNCOP_1:53; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: 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
let F, G be BinOp of D; ::_thesis: ( F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies (G [:] ((id D),d)) . (the_unity_wrt F) = the_unity_wrt F )
assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp and
A4: G is_distributive_wrt F ; ::_thesis: (G [:] ((id D),d)) . (the_unity_wrt F) = the_unity_wrt F
set e = the_unity_wrt F;
set i = the_inverseOp_wrt F;
G . ((the_unity_wrt F),d) = G . ((F . ((the_unity_wrt F),(the_unity_wrt F))),d) by A2, SETWISEO:15
.= F . ((G . ((the_unity_wrt F),d)),(G . ((the_unity_wrt F),d))) by A4, BINOP_1:11 ;
then  the_unity_wrt F = F . ((F . ((G . ((the_unity_wrt F),d)),(G . ((the_unity_wrt F),d)))),((the_inverseOp_wrt F) . (G . ((the_unity_wrt F),d)))) by A1, A2, A3, Th59;
then  the_unity_wrt F = F . ((G . ((the_unity_wrt F),d)),(F . ((G . ((the_unity_wrt F),d)),((the_inverseOp_wrt F) . (G . ((the_unity_wrt F),d)))))) by A1, BINOP_1:def_3;
then  the_unity_wrt F = F . ((G . ((the_unity_wrt F),d)),(the_unity_wrt F)) by A1, A2, A3, Th59;
then  the_unity_wrt F = G . ((the_unity_wrt F),d) by A2, SETWISEO:15;
then  G . (((id D) . (the_unity_wrt F)),d) = the_unity_wrt F by FUNCT_1:18;
hence  (G [:] ((id D),d)) . (the_unity_wrt F) = the_unity_wrt F by FUNCOP_1:48; ::_thesis: verum
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) )
proof
let D, C be non empty set ; ::_thesis: 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) )
let f be Function of C,D; ::_thesis: 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) )
let F be BinOp of D; ::_thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp implies ( F .: (f,((the_inverseOp_wrt F) * f)) = C --> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * f),f) = C --> (the_unity_wrt F) ) )
set u = the_inverseOp_wrt F;
reconsider g = C --> (the_unity_wrt F) as Function of C,D ;
assume A1: ( F is having_a_unity & F is associative & F is having_an_inverseOp ) ; ::_thesis: ( F .: (f,((the_inverseOp_wrt F) * f)) = C --> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * f),f) = C --> (the_unity_wrt F) )
now__::_thesis:_for_c_being_Element_of_C_holds_(F_.:_(f,((the_inverseOp_wrt_F)_*_f)))_._c_=_g_._c
let c be Element of C; ::_thesis: (F .: (f,((the_inverseOp_wrt F) * f))) . c = g . c
thus (F .: (f,((the_inverseOp_wrt F) * f))) . c = F . ((f . c),(((the_inverseOp_wrt F) * f) . c)) by FUNCOP_1:37
.= F . ((f . c),((the_inverseOp_wrt F) . (f . c))) by FUNCT_2:15
.= the_unity_wrt F by A1, Th59
.= g . c by FUNCOP_1:7 ; ::_thesis: verum
end;
hence  F .: (f,((the_inverseOp_wrt F) * f)) = C --> (the_unity_wrt F) by FUNCT_2:63; ::_thesis: F .: (((the_inverseOp_wrt F) * f),f) = C --> (the_unity_wrt F)
now__::_thesis:_for_c_being_Element_of_C_holds_(F_.:_(((the_inverseOp_wrt_F)_*_f),f))_._c_=_g_._c
let c be Element of C; ::_thesis: (F .: (((the_inverseOp_wrt F) * f),f)) . c = g . c
thus (F .: (((the_inverseOp_wrt F) * f),f)) . c = F . ((((the_inverseOp_wrt F) * f) . c),(f . c)) by FUNCOP_1:37
.= F . (((the_inverseOp_wrt F) . (f . c)),(f . c)) by FUNCT_2:15
.= the_unity_wrt F by A1, Th59
.= g . c by FUNCOP_1:7 ; ::_thesis: verum
end;
hence  F .: (((the_inverseOp_wrt F) * f),f) = C --> (the_unity_wrt F) by FUNCT_2:63; ::_thesis: verum
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 )
proof
let D, C be non empty set ; ::_thesis: 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 )
let f, f9 be Function of C,D; ::_thesis: 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 )
let F be BinOp of D; ::_thesis: ( F is associative & F is having_an_inverseOp & F is having_a_unity & F .: (f,f9) = C --> (the_unity_wrt F) implies ( f = (the_inverseOp_wrt F) * f9 & (the_inverseOp_wrt F) * f = f9 ) )
assume that
A1: ( F is associative & F is having_an_inverseOp & F is having_a_unity ) and
A2: F .: (f,f9) = C --> (the_unity_wrt F) ; ::_thesis: ( f = (the_inverseOp_wrt F) * f9 & (the_inverseOp_wrt F) * f = f9 )
set u = the_inverseOp_wrt F;
set e = the_unity_wrt F;
reconsider g = C --> (the_unity_wrt F) as Function of C,D ;
now__::_thesis:_for_c_being_Element_of_C_holds_f_._c_=_((the_inverseOp_wrt_F)_*_f9)_._c
let c be Element of C; ::_thesis: f . c = ((the_inverseOp_wrt F) * f9) . c
F . ((f . c),(f9 . c)) = g . c by A2, FUNCOP_1:37
.= the_unity_wrt F by FUNCOP_1:7 ;
hence f . c = (the_inverseOp_wrt F) . (f9 . c) by A1, Th60
.= ((the_inverseOp_wrt F) * f9) . c by FUNCT_2:15 ;
::_thesis: verum
end;
hence  f = (the_inverseOp_wrt F) * f9 by FUNCT_2:63; ::_thesis: (the_inverseOp_wrt F) * f = f9
now__::_thesis:_for_c_being_Element_of_C_holds_((the_inverseOp_wrt_F)_*_f)_._c_=_f9_._c
let c be Element of C; ::_thesis: ((the_inverseOp_wrt F) * f) . c = f9 . c
F . ((f . c),(f9 . c)) = g . c by A2, FUNCOP_1:37
.= the_unity_wrt F by FUNCOP_1:7 ;
then  f9 . c = (the_inverseOp_wrt F) . (f . c) by A1, Th60;
hence  ((the_inverseOp_wrt F) * f) . c = f9 . c by FUNCT_2:15; ::_thesis: verum
end;
hence  (the_inverseOp_wrt F) * f = f9 by FUNCT_2:63; ::_thesis: verum
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) )
proof
let D be non empty set ; ::_thesis: 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) )
let i be Nat; ::_thesis: 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) )
let T be Tuple of i,D; ::_thesis: 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) )
let F be BinOp of D; ::_thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp implies ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) ) )
assume A1: ( F is having_a_unity & F is associative & F is having_an_inverseOp ) ; ::_thesis: ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) )
reconsider uT = (the_inverseOp_wrt F) * T as Element of i -tuples_on D by FINSEQ_2:113;
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) )
then  ( F .: (T,uT) = <*> D & F .: (uT,T) = <*> D ) by Lm1;
hence  ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) ) by A2; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) )
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  ( F .: (T,((the_inverseOp_wrt F) * T)) = i |-> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * T),T) = i |-> (the_unity_wrt F) ) by A1, Th71; ::_thesis: verum
end;
end;
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 )
proof
let D be non empty set ; ::_thesis: 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 )
let i be Nat; ::_thesis: 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 )
let T1, T2 be Tuple of i,D; ::_thesis: 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 )
let F be BinOp of D; ::_thesis: ( F is associative & F is having_an_inverseOp & F is having_a_unity & F .: (T1,T2) = i |-> (the_unity_wrt F) implies ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 ) )
assume A1: ( F is associative & F is having_an_inverseOp & F is having_a_unity & F .: (T1,T2) = i |-> (the_unity_wrt F) ) ; ::_thesis: ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 )
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 )
then  ( T1 = <*> D & T2 = <*> D ) ;
hence  ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 ) ; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 )
then reconsider C = Seg i as non empty set ;
 ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4;
hence  ( T1 = (the_inverseOp_wrt F) * T2 & (the_inverseOp_wrt F) * T1 = T2 ) by A1, Th72; ::_thesis: verum
end;
end;
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
proof
let D, C be non empty set ; ::_thesis: 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
let e be Element of D; ::_thesis: 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
let f be Function of C,D; ::_thesis: 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
let F, G be BinOp of D; ::_thesis: ( F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F implies G [;] (e,f) = C --> e )
reconsider g = C --> e as Function of C,D ;
assume A1: ( F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F ) ; ::_thesis: G [;] (e,f) = C --> e
now__::_thesis:_for_c_being_Element_of_C_holds_(G_[;]_(e,f))_._c_=_g_._c
let c be Element of C; ::_thesis: (G [;] (e,f)) . c = g . c
thus (G [;] (e,f)) . c = G . (e,(f . c)) by FUNCOP_1:53
.= e by A1, Th66
.= g . c by FUNCOP_1:7 ; ::_thesis: verum
end;
hence  G [;] (e,f) = C --> e by FUNCT_2:63; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let e be Element of D; ::_thesis: 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
let i be Nat; ::_thesis: 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
let T be Tuple of i,D; ::_thesis: 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
let F, G be BinOp of D; ::_thesis: ( F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F implies G [;] (e,T) = i |-> e )
assume A1: ( F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F ) ; ::_thesis: G [;] (e,T) = i |-> e
percases ( i = 0 or i <> 0 ) ;
supposeA2: i = 0 ; ::_thesis: G [;] (e,T) = i |-> e
then  G [;] (e,T) = <*> D by Lm2;
hence  G [;] (e,T) = i |-> e by A2; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: G [;] (e,T) = i |-> e
then reconsider C = Seg i as non empty set ;
 T is Function of C,D by Lm4;
hence  G [;] (e,T) = i |-> e by A1, Th75; ::_thesis: verum
end;
end;
end;

definition
let F, f, g be Function;
funcF * (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 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))
proof
let x, y be set ; ::_thesis: 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))
let F, f, g be Function; ::_thesis: ( [x,y] in dom (F * (f,g)) implies (F * (f,g)) . (x,y) = F . ((f . x),(g . y)) )
assume A1: [x,y] in dom (F * (f,g)) ; ::_thesis: (F * (f,g)) . (x,y) = F . ((f . x),(g . y))
 [x,y] in dom [:f,g:] by A1, FUNCT_1:11;
then  [x,y] in [:(dom f),(dom g):] by FUNCT_3:def_8;
then  [:f,g:] . (x,y) = [(f . x),(g . y)] by FUNCT_3:65;
hence  (F * (f,g)) . (x,y) = F . ((f . x),(g . y)) by A1, FUNCT_1:12; ::_thesis: verum
end;

theorem :: FINSEQOP:78
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 Th77;

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
proof
let D, D9, E, C, C9 be non empty set ; ::_thesis: 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
let F be Function of [:D,D9:],E; ::_thesis: for f being Function of C,D
for g being Function of C9,D9 holds F * (f,g) is Function of [:C,C9:],E
let f be Function of C,D; ::_thesis: for g being Function of C9,D9 holds F * (f,g) is Function of [:C,C9:],E
let g be Function of C9,D9; ::_thesis: F * (f,g) is Function of [:C,C9:],E
 F * (f,g) = F * [:f,g:] ;
hence  F * (f,g) is Function of [:C,C9:],E ; ::_thesis: verum
end;

theorem :: FINSEQOP:80
for D being non empty set
for F being BinOp of D
for u, u9 being Function of D,D holds F * (u,u9) is BinOp of D by Th79;

definition
let D be non empty set ;
let F be BinOp of D;
let f, f9 be Function of D,D;
:: original: *
redefine funcF * (f,f9) ->  BinOp of D;
coherence
 F * (f,f9) is BinOp of D by Th79;
end;

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))
proof
let D, D9, E, C, C9 be non empty set ; ::_thesis: 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))
let c be Element of C; ::_thesis: 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))
let c9 be Element of C9; ::_thesis: 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))
let F be Function of [:D,D9:],E; ::_thesis: 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))
let f be Function of C,D; ::_thesis: for g being Function of C9,D9 holds (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9))
let g be Function of C9,D9; ::_thesis: (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9))
set H = F * (f,g);
 F * (f,g) is Function of [:C,C9:],E by Th79;
then  dom (F * (f,g)) = [:C,C9:] by FUNCT_2:def_1;
then  [c,c9] in dom (F * (f,g)) by ZFMISC_1:def_2;
hence  (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9)) by Th77; ::_thesis: verum
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) )
proof
let D be non empty set ; ::_thesis: 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) )
let d1, d2 be Element of D; ::_thesis: 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) )
let F be BinOp of D; ::_thesis: 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) )
let u be Function of D,D; ::_thesis: ( (F * ((id D),u)) . (d1,d2) = F . (d1,(u . d2)) & (F * (u,(id D))) . (d1,d2) = F . ((u . d1),d2) )
 ( (id D) . d1 = d1 & (id D) . d2 = d2 ) by FUNCT_1:18;
hence  ( (F * ((id D),u)) . (d1,d2) = F . (d1,(u . d2)) & (F * (u,(id D))) . (d1,d2) = F . ((u . d1),d2) ) by Th81; ::_thesis: verum
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))
proof
let C, D be non empty set ; ::_thesis: 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))
let f, f9 be Function of C,D; ::_thesis: for F being BinOp of D
for u being UnOp of D holds (F * ((id D),u)) .: (f,f9) = F .: (f,(u * f9))
let F be BinOp of D; ::_thesis: for u being UnOp of D holds (F * ((id D),u)) .: (f,f9) = F .: (f,(u * f9))
let u be UnOp of D; ::_thesis: (F * ((id D),u)) .: (f,f9) = F .: (f,(u * f9))
now__::_thesis:_for_c_being_Element_of_C_holds_((F_*_((id_D),u))_.:_(f,f9))_._c_=_(F_.:_(f,(u_*_f9)))_._c
let c be Element of C; ::_thesis: ((F * ((id D),u)) .: (f,f9)) . c = (F .: (f,(u * f9))) . c
thus ((F * ((id D),u)) .: (f,f9)) . c = (F * ((id D),u)) . ((f . c),(f9 . c)) by FUNCOP_1:37
.= F . ((f . c),(u . (f9 . c))) by Th82
.= F . ((f . c),((u * f9) . c)) by FUNCT_2:15
.= (F .: (f,(u * f9))) . c by FUNCOP_1:37 ; ::_thesis: verum
end;
hence  (F * ((id D),u)) .: (f,f9) = F .: (f,(u * f9)) by FUNCT_2:63; ::_thesis: verum
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))
proof
let D be non empty set ; ::_thesis: 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))
let i be Nat; ::_thesis: 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))
let T1, T2 be Tuple of i,D; ::_thesis: for F being BinOp of D
for u being UnOp of D holds (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2))
let F be BinOp of D; ::_thesis: for u being UnOp of D holds (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2))
let u be UnOp of D; ::_thesis: (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2))
now__::_thesis:_(F_*_((id_D),u))_.:_(T1,T2)_=_F_.:_(T1,(u_*_T2))
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2))
then  ( (F * ((id D),u)) .: (T1,T2) = <*> D & u * T2 = <*> D ) by Lm1;
hence  (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) by FINSEQ_2:73; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2))
then reconsider C = Seg i as non empty set ;
 ( T1 is Function of C,D & T2 is Function of C,D ) by Lm4;
hence  (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) by Th83; ::_thesis: verum
end;
end;
end;
hence  (F * ((id D),u)) .: (T1,T2) = F .: (T1,(u * T2)) ; ::_thesis: verum
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)) )
proof
let D be non empty set ; ::_thesis: 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)) )
let d1, d2 be Element of D; ::_thesis: 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)) )
let F be BinOp of D; ::_thesis: 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)) )
let u be UnOp of D; ::_thesis: ( F is associative & F is having_a_unity & F is commutative & F is having_an_inverseOp & u = the_inverseOp_wrt F implies ( 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)) ) )
assume that
A1: ( F is associative & F is having_a_unity ) and
A2: F is commutative and
A3: ( F is having_an_inverseOp & u = the_inverseOp_wrt F ) ; ::_thesis: ( 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)) )
A4: u is_distributive_wrt F by A1, A2, A3, Th63;
thus u . ((F * ((id D),u)) . (d1,d2)) = u . (F . (d1,(u . d2))) by Th82
.= F . ((u . d1),(u . (u . d2))) by A4, BINOP_1:def_12
.= F . ((u . d1),d2) by A1, A3, Th62
.= (F * (u,(id D))) . (d1,d2) by Th82 ; ::_thesis: (F * ((id D),u)) . (d1,d2) = u . ((F * (u,(id D))) . (d1,d2))
hence  (F * ((id D),u)) . (d1,d2) = u . ((F * (u,(id D))) . (d1,d2)) by A1, A3, Th62; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: 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
let F be BinOp of D; ::_thesis: ( F is associative & F is having_a_unity & F is having_an_inverseOp implies (F * ((id D),(the_inverseOp_wrt F))) . (d,d) = the_unity_wrt F )
assume A1: ( F is associative & F is having_a_unity & F is having_an_inverseOp ) ; ::_thesis: (F * ((id D),(the_inverseOp_wrt F))) . (d,d) = the_unity_wrt F
set u = the_inverseOp_wrt F;
thus (F * ((id D),(the_inverseOp_wrt F))) . (d,d) = F . (d,((the_inverseOp_wrt F) . d)) by Th82
.= the_unity_wrt F by A1, Th59 ; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: 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
let F be BinOp of D; ::_thesis: ( F is associative & F is having_a_unity & F is having_an_inverseOp implies (F * ((id D),(the_inverseOp_wrt F))) . (d,(the_unity_wrt F)) = d )
assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp ; ::_thesis: (F * ((id D),(the_inverseOp_wrt F))) . (d,(the_unity_wrt F)) = d
set u = the_inverseOp_wrt F;
set e = the_unity_wrt F;
thus (F * ((id D),(the_inverseOp_wrt F))) . (d,(the_unity_wrt F)) = F . (d,((the_inverseOp_wrt F) . (the_unity_wrt F))) by Th82
.= F . (d,(the_unity_wrt F)) by A1, A2, A3, Th61
.= d by A2, SETWISEO:15 ; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let d be Element of D; ::_thesis: 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
let F be BinOp of D; ::_thesis: for u being UnOp of D st F is having_a_unity holds
(F * ((id D),u)) . ((the_unity_wrt F),d) = u . d
let u be UnOp of D; ::_thesis: ( F is having_a_unity implies (F * ((id D),u)) . ((the_unity_wrt F),d) = u . d )
assume A1: F is having_a_unity ; ::_thesis: (F * ((id D),u)) . ((the_unity_wrt F),d) = u . d
set e = the_unity_wrt F;
thus (F * ((id D),u)) . ((the_unity_wrt F),d) = F . ((the_unity_wrt F),(u . d)) by Th82
.= u . d by A1, SETWISEO:15 ; ::_thesis: verum
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)))
proof
let D be non empty set ; ::_thesis: 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)))
let F, G be BinOp of D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G = F * ((id D),(the_inverseOp_wrt F)) implies for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) )
assume that
A1: F is commutative and
A2: F is associative and
A3: ( F is having_a_unity & F is having_an_inverseOp ) and
A4: G = F * ((id D),(the_inverseOp_wrt F)) ; ::_thesis: for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4)))
set u = the_inverseOp_wrt F;
A5: the_inverseOp_wrt F is_distributive_wrt F by A1, A2, A3, Th63;
let d1, d2, d3, d4 be Element of D; ::_thesis: F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4)))
thus F . ((G . (d1,d2)),(G . (d3,d4))) = F . ((F . (d1,((the_inverseOp_wrt F) . d2))),(G . (d3,d4))) by A4, Th82
.= F . ((F . (d1,((the_inverseOp_wrt F) . d2))),(F . (d3,((the_inverseOp_wrt F) . d4)))) by A4, Th82
.= F . (d1,(F . (((the_inverseOp_wrt F) . d2),(F . (d3,((the_inverseOp_wrt F) . d4)))))) by A2, BINOP_1:def_3
.= F . (d1,(F . ((F . (((the_inverseOp_wrt F) . d2),d3)),((the_inverseOp_wrt F) . d4)))) by A2, BINOP_1:def_3
.= F . (d1,(F . ((F . (d3,((the_inverseOp_wrt F) . d2))),((the_inverseOp_wrt F) . d4)))) by A1, BINOP_1:def_2
.= F . (d1,(F . (d3,(F . (((the_inverseOp_wrt F) . d2),((the_inverseOp_wrt F) . d4)))))) by A2, BINOP_1:def_3
.= F . ((F . (d1,d3)),(F . (((the_inverseOp_wrt F) . d2),((the_inverseOp_wrt F) . d4)))) by A2, BINOP_1:def_3
.= F . ((F . (d1,d3)),((the_inverseOp_wrt F) . (F . (d2,d4)))) by A5, BINOP_1:def_12
.= G . ((F . (d1,d3)),(F . (d2,d4))) by A4, Th82 ; ::_thesis: verum
end;