:: SETWOP_2 semantic presentation

begin

                                     Lm1:  for i being Nat holds Seg i is Element of Fin NAT
by FINSUB_1:def_5;

Lm2: now__::_thesis:_for_i_being_Nat_holds_not_i_+_1_in_Seg_i
let i be Nat; ::_thesis: not i + 1 in Seg i
assume  i + 1 in Seg i ; ::_thesis: contradiction
then  i + 1 <= i by FINSEQ_1:1;
hence  contradiction by XREAL_1:29; ::_thesis: verum
end;

theorem Th1: :: SETWOP_2:1
for C, D being non empty set
for c1, c2 being Element of C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & c1 <> c2 holds
F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))
proof
let C, D be non empty set ; ::_thesis: for c1, c2 being Element of C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & c1 <> c2 holds
F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))
let c1, c2 be Element of C; ::_thesis: for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & c1 <> c2 holds
F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))
let F be BinOp of D; ::_thesis: for f being Function of C,D st F is commutative & F is associative & c1 <> c2 holds
F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))
let f be Function of C,D; ::_thesis: ( F is commutative & F is associative & c1 <> c2 implies F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2)) )
assume that
A1: ( F is commutative & F is associative ) and
A2: c1 <> c2 ; ::_thesis: F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))
consider g being Function of (Fin C),D such that
A3: F $$ ({.c1,c2.},f) = g . {c1,c2} and
 for e being Element of D st e is_a_unity_wrt F holds
g . {} = e and
A4: for c being Element of C holds g . {c} = f . c and
A5: for B being Element of Fin C st B c= {c1,c2} & B <> {} holds
for c being Element of C st c in {c1,c2} \ B holds
g . (B \/ {c}) = F . ((g . B),(f . c)) by A1, SETWISEO:def_3;
 ( c1 in {c1} & not c2 in {c1} ) by A2, TARSKI:def_1;
then  {c1,c2} \ {c1} = {c2} by ZFMISC_1:62;
then A6: c2 in {c1,c2} \ {c1} by TARSKI:def_1;
thus F $$ ({.c1,c2.},f) = g . ({.c1.} \/ {.c2.}) by A3, ENUMSET1:1
.= F . ((g . {c1}),(f . c2)) by A5, A6, ZFMISC_1:7
.= F . ((f . c1),(f . c2)) by A4 ; ::_thesis: verum
end;

theorem Th2: :: SETWOP_2:2
for C, D being non empty set
for c being Element of C
for B being Element of Fin C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds
F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))
proof
let C, D be non empty set ; ::_thesis: for c being Element of C
for B being Element of Fin C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds
F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))
let c be Element of C; ::_thesis: for B being Element of Fin C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds
F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))
let B be Element of Fin C; ::_thesis: for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds
F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))
let F be BinOp of D; ::_thesis: for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds
F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))
let f be Function of C,D; ::_thesis: ( F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B implies F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c)) )
assume that
A1: ( F is commutative & F is associative ) and
A2: ( B <> {} or F is having_a_unity ) and
A3: not c in B ; ::_thesis: F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))
percases ( B = {} or B <> {} ) ;
supposeA4: B = {} ; ::_thesis: F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))
then  B = {}. C ;
then  F $$ (B,f) = the_unity_wrt F by A1, A2, SETWISEO:31;
hence F . ((F $$ (B,f)),(f . c)) = f . c by A2, A4, SETWISEO:15
.= F $$ ((B \/ {.c.}),f) by A1, A4, SETWISEO:17 ;
::_thesis: verum
end;
supposeA5: B <> {} ; ::_thesis: F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))
consider g9 being Function of (Fin C),D such that
A6: F $$ (B,f) = g9 . B and
 for e being Element of D st e is_a_unity_wrt F holds
g9 . {} = e and
A7: for c9 being Element of C holds g9 . {c9} = f . c9 and
A8: for B9 being Element of Fin C st B9 c= B & B9 <> {} holds
for c9 being Element of C st c9 in B \ B9 holds
g9 . (B9 \/ {c9}) = F . ((g9 . B9),(f . c9)) by A1, A2, SETWISEO:def_3;
consider g being Function of (Fin C),D such that
A9: F $$ ((B \/ {.c.}),f) = g . (B \/ {c}) and
 for e being Element of D st e is_a_unity_wrt F holds
g . {} = e and
A10: for c9 being Element of C holds g . {c9} = f . c9 and
A11: for B9 being Element of Fin C st B9 c= B \/ {c} & B9 <> {} holds
for c9 being Element of C st c9 in (B \/ {c}) \ B9 holds
g . (B9 \/ {c9}) = F . ((g . B9),(f . c9)) by A1, SETWISEO:def_3;
defpred S1[ set ] means ( $1 <> {} & $1 c= B implies g . $1 = g9 . $1 );
A12: for B9 being Element of Fin C
for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
proof
A13: B c= B \/ {c} by XBOOLE_1:7;
let B9 be Element of Fin C; ::_thesis: for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
let c9 be Element of C; ::_thesis: ( S1[B9] & not c9 in B9 implies S1[B9 \/ {c9}] )
assume that
A14: ( B9 <> {} & B9 c= B implies g . B9 = g9 . B9 ) and
A15: not c9 in B9 and
 B9 \/ {c9} <> {} and
A16: B9 \/ {c9} c= B ; ::_thesis: g . (B9 \/ {c9}) = g9 . (B9 \/ {c9})
A17: c9 in B by A16, ZFMISC_1:137;
then A18: c9 in B \ B9 by A15, XBOOLE_0:def_5;
 c9 in B \/ {c} by A17, XBOOLE_0:def_3;
then A19: c9 in (B \/ {c}) \ B9 by A15, XBOOLE_0:def_5;
 B9 c= B by A16, XBOOLE_1:11;
then A20: B9 c= B \/ {c} by A13, XBOOLE_1:1;
percases ( B9 = {} or B9 <> {} ) ;
supposeA21: B9 = {} ; ::_thesis: g . (B9 \/ {c9}) = g9 . (B9 \/ {c9})
then  g . (B9 \/ {c9}) = f . c9 by A10;
hence  g . (B9 \/ {c9}) = g9 . (B9 \/ {c9}) by A7, A21; ::_thesis: verum
end;
supposeA22: B9 <> {} ; ::_thesis: g . (B9 \/ {c9}) = g9 . (B9 \/ {c9})
hence g . (B9 \/ {c9}) = F . ((g9 . B9),(f . c9)) by A11, A14, A16, A20, A19, XBOOLE_1:11
.= g9 . (B9 \/ {c9}) by A8, A16, A18, A22, XBOOLE_1:11 ;
::_thesis: verum
end;
end;
end;
A23: S1[ {}. C] ;
A24: for B9 being Element of Fin C holds S1[B9] from SETWISEO:sch_2(A23, A12);
 c in B \/ {c} by ZFMISC_1:136;
then  c in (B \/ {c}) \ B by A3, XBOOLE_0:def_5;
hence F $$ ((B \/ {.c.}),f) = F . ((g . B),(f . c)) by A5, A9, A11, XBOOLE_1:7
.= F . ((F $$ (B,f)),(f . c)) by A5, A6, A24 ;
::_thesis: verum
end;
end;
end;

theorem :: SETWOP_2:3
for C, D being non empty set
for c1, c2, c3 being Element of C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & c1 <> c2 & c1 <> c3 & c2 <> c3 holds
F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3))
proof
let C, D be non empty set ; ::_thesis: for c1, c2, c3 being Element of C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & c1 <> c2 & c1 <> c3 & c2 <> c3 holds
F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3))
let c1, c2, c3 be Element of C; ::_thesis: for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & c1 <> c2 & c1 <> c3 & c2 <> c3 holds
F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3))
let F be BinOp of D; ::_thesis: for f being Function of C,D st F is commutative & F is associative & c1 <> c2 & c1 <> c3 & c2 <> c3 holds
F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3))
let f be Function of C,D; ::_thesis: ( F is commutative & F is associative & c1 <> c2 & c1 <> c3 & c2 <> c3 implies F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3)) )
assume that
A1: ( F is commutative & F is associative ) and
A2: c1 <> c2 ; ::_thesis: ( not c1 <> c3 or not c2 <> c3 or F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3)) )
assume  ( c1 <> c3 & c2 <> c3 ) ; ::_thesis: F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3))
then A3: not c3 in {c1,c2} by TARSKI:def_2;
thus F $$ ({.c1,c2,c3.},f) = F $$ (({.c1,c2.} \/ {.c3.}),f) by ENUMSET1:3
.= F . ((F $$ ({.c1,c2.},f)),(f . c3)) by A1, A3, Th2
.= F . ((F . ((f . c1),(f . c2))),(f . c3)) by A1, A2, Th1 ; ::_thesis: verum
end;

theorem :: SETWOP_2:4
for C, D being non empty set
for B1, B2 being Element of Fin C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
proof
let C, D be non empty set ; ::_thesis: for B1, B2 being Element of Fin C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
let B1, B2 be Element of Fin C; ::_thesis: for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
let F be BinOp of D; ::_thesis: for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
let f be Function of C,D; ::_thesis: ( F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 implies F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) )
assume that
A1: ( F is commutative & F is associative ) and
A2: ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) and
A3: B1 /\ B2 = {} ; :: according to XBOOLE_0:def_7 ::_thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
now__::_thesis:_F_$$_((B1_\/_B2),f)_=_F_._((F_$$_(B1,f)),(F_$$_(B2,f)))
percases ( B1 = {} or B2 = {} or ( B1 <> {} & B2 <> {} ) ) ;
supposeA4: ( B1 = {} or B2 = {} ) ; ::_thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
now__::_thesis:_F_$$_((B1_\/_B2),f)_=_F_._((F_$$_(B1,f)),(F_$$_(B2,f)))
percases ( B1 = {} or B2 = {} ) by A4;
supposeA5: B1 = {} ; ::_thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
hence F $$ ((B1 \/ B2),f) = F . ((the_unity_wrt F),(F $$ (B2,f))) by A2, SETWISEO:15
.= F . ((F $$ (({}. C),f)),(F $$ (B2,f))) by A1, A2, A4, SETWISEO:31
.= F . ((F $$ (B1,f)),(F $$ (B2,f))) by A5 ;
::_thesis: verum
end;
supposeA6: B2 = {} ; ::_thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
hence F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(the_unity_wrt F)) by A2, SETWISEO:15
.= F . ((F $$ (B1,f)),(F $$ (({}. C),f))) by A1, A2, A4, SETWISEO:31
.= F . ((F $$ (B1,f)),(F $$ (B2,f))) by A6 ;
::_thesis: verum
end;
end;
end;
hence  F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) ; ::_thesis: verum
end;
supposeA7: ( B1 <> {} & B2 <> {} ) ; ::_thesis: F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
defpred S1[ Element of Fin C] means ( $1 <> {} & B1 /\ $1 = {} implies F $$ ((B1 \/ $1),f) = F . ((F $$ (B1,f)),(F $$ ($1,f))) );
A8: for B9 being Element of Fin C
for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
proof
let B be Element of Fin C; ::_thesis: for b being Element of C st S1[B] & not b in B holds
S1[B \/ {.b.}]
let c be Element of C; ::_thesis: ( S1[B] & not c in B implies S1[B \/ {.c.}] )
assume that
A9: ( B <> {} & B1 /\ B = {} implies F $$ ((B1 \/ B),f) = F . ((F $$ (B1,f)),(F $$ (B,f))) ) and
A10: not c in B and
 B \/ {c} <> {} ; ::_thesis: ( not B1 /\ (B \/ {.c.}) = {} or F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f))) )
assume A11: B1 /\ (B \/ {c}) = {} ; ::_thesis: F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))
then A12: B1 misses B \/ {c} by XBOOLE_0:def_7;
 c in B \/ {c} by ZFMISC_1:136;
then A13: not c in B1 by A11, XBOOLE_0:def_4;
A14: ( B <> {} & B1 misses B implies F $$ ((B1 \/ B),f) = F . ((F $$ (B1,f)),(F $$ (B,f))) ) by A9, XBOOLE_0:def_7;
now__::_thesis:_F_$$_((B1_\/_(B_\/_{.c.})),f)_=_F_._((F_$$_(B1,f)),(F_$$_((B_\/_{.c.}),f)))
percases ( B = {} or B <> {} ) ;
supposeA15: B = {} ; ::_thesis: F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))
hence F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(f . c)) by A1, A7, A13, Th2
.= F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f))) by A1, A15, SETWISEO:17 ;
::_thesis: verum
end;
supposeA16: B <> {} ; ::_thesis: F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))
A17: not c in B1 \/ B by A10, A13, XBOOLE_0:def_3;
thus F $$ ((B1 \/ (B \/ {.c.})),f) = F $$ (((B1 \/ B) \/ {.c.}),f) by XBOOLE_1:4
.= F . ((F . ((F $$ (B1,f)),(F $$ (B,f)))),(f . c)) by A1, A14, A12, A16, A17, Th2, XBOOLE_1:7, XBOOLE_1:63
.= F . ((F $$ (B1,f)),(F . ((F $$ (B,f)),(f . c)))) by A1, BINOP_1:def_3
.= F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f))) by A1, A10, A16, Th2 ; ::_thesis: verum
end;
end;
end;
hence  F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f))) ; ::_thesis: verum
end;
A18: S1[ {}. C] ;
 for B2 being Element of Fin C holds S1[B2] from SETWISEO:sch_2(A18, A8);
hence  F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) by A3, A7; ::_thesis: verum
end;
end;
end;
hence  F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) ; ::_thesis: verum
end;

theorem Th5: :: SETWOP_2:5
for C, C9, D being non empty set
for B being Element of Fin C
for A being Element of Fin C9
for F being BinOp of D
for f being Function of C,D
for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds
F $$ (A,g) = F $$ (B,f)
proof
let C, C9, D be non empty set ; ::_thesis: for B being Element of Fin C
for A being Element of Fin C9
for F being BinOp of D
for f being Function of C,D
for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds
F $$ (A,g) = F $$ (B,f)
let B be Element of Fin C; ::_thesis: for A being Element of Fin C9
for F being BinOp of D
for f being Function of C,D
for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds
F $$ (A,g) = F $$ (B,f)
let A be Element of Fin C9; ::_thesis: for F being BinOp of D
for f being Function of C,D
for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds
F $$ (A,g) = F $$ (B,f)
let F be BinOp of D; ::_thesis: for f being Function of C,D
for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds
F $$ (A,g) = F $$ (B,f)
let f be Function of C,D; ::_thesis: for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds
F $$ (A,g) = F $$ (B,f)
let g be Function of C9,D; ::_thesis: ( F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) implies F $$ (A,g) = F $$ (B,f) )
defpred S1[ Element of Fin C9] means ( ( $1 <> {} or F is having_a_unity ) implies for B being Element of Fin C st ex s being Function st
( dom s = $1 & rng s = B & s is one-to-one & g | $1 = f * s ) holds
F $$ ($1,g) = F $$ (B,f) );
assume A1: ( F is commutative & F is associative ) ; ::_thesis: ( ( not A <> {} & not F is having_a_unity ) or for s being Function holds
( not dom s = A or not rng s = B or not s is one-to-one or not g | A = f * s ) or F $$ (A,g) = F $$ (B,f) )
A2: for B9 being Element of Fin C9
for b being Element of C9 st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
proof
let A9 be Element of Fin C9; ::_thesis: for b being Element of C9 st S1[A9] & not b in A9 holds
S1[A9 \/ {.b.}]
let a be Element of C9; ::_thesis: ( S1[A9] & not a in A9 implies S1[A9 \/ {.a.}] )
assume that
A3: ( ( A9 <> {} or F is having_a_unity ) implies for B being Element of Fin C st ex s being Function st
( dom s = A9 & rng s = B & s is one-to-one & g | A9 = f * s ) holds
F $$ (A9,g) = F $$ (B,f) ) and
A4: not a in A9 ; ::_thesis: S1[A9 \/ {.a.}]
assume  ( A9 \/ {a} <> {} or F is having_a_unity ) ; ::_thesis: for B being Element of Fin C st ex s being Function st
( dom s = A9 \/ {.a.} & rng s = B & s is one-to-one & g | (A9 \/ {.a.}) = f * s ) holds
F $$ ((A9 \/ {.a.}),g) = F $$ (B,f)
let B be Element of Fin C; ::_thesis: ( ex s being Function st
( dom s = A9 \/ {.a.} & rng s = B & s is one-to-one & g | (A9 \/ {.a.}) = f * s ) implies F $$ ((A9 \/ {.a.}),g) = F $$ (B,f) )
set A = A9 \/ {.a.};
given s being Function such that A5: dom s = A9 \/ {.a.} and
A6: rng s = B and
A7: s is one-to-one and
A8: g | (A9 \/ {.a.}) = f * s ; ::_thesis: F $$ ((A9 \/ {.a.}),g) = F $$ (B,f)
A9: a in A9 \/ {.a.} by ZFMISC_1:136;
then A10: s . a in B by A5, A6, FUNCT_1:def_3;
 B c= C by FINSUB_1:def_5;
then reconsider c = s . a as Element of C by A10;
set B9 = B \ {.c.};
set s9 = s | A9;
A11: s | A9 is one-to-one by A7, FUNCT_1:52;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_rng_(s_|_A9)_implies_y_in_B_\_{.c.}_)_&_(_y_in_B_\_{.c.}_implies_y_in_rng_(s_|_A9)_)_)
let y be set ; ::_thesis: ( ( y in rng (s | A9) implies y in B \ {.c.} ) & ( y in B \ {.c.} implies y in rng (s | A9) ) )
thus  ( y in rng (s | A9) implies y in B \ {.c.} ) ::_thesis: ( y in B \ {.c.} implies y in rng (s | A9) )
proof
assume  y in rng (s | A9) ; ::_thesis: y in B \ {.c.}
then consider x being set  such that
A12: x in dom (s | A9) and
A13: y = (s | A9) . x by FUNCT_1:def_3;
A14: (s | A9) . x = s . x by A12, FUNCT_1:47;
A15: x in (dom s) /\ A9 by A12, RELAT_1:61;
then  ( x in dom s & x <> a ) by A4, XBOOLE_0:def_4;
then  s . x <> c by A5, A7, A9, FUNCT_1:def_4;
then A16: not y in {c} by A13, A14, TARSKI:def_1;
 x in dom s by A15, XBOOLE_0:def_4;
then  y in B by A6, A13, A14, FUNCT_1:def_3;
hence  y in B \ {.c.} by A16, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A17: y in B \ {.c.} ; ::_thesis: y in rng (s | A9)
then  y in B by XBOOLE_0:def_5;
then consider x being set  such that
A18: x in dom s and
A19: y = s . x by A6, FUNCT_1:def_3;
A20: ( x in A9 or x in {a} ) by A5, A18, XBOOLE_0:def_3;
 not y in {c} by A17, XBOOLE_0:def_5;
then  x <> a by A19, TARSKI:def_1;
then  x in (dom s) /\ A9 by A18, A20, TARSKI:def_1, XBOOLE_0:def_4;
then  ( x in dom (s | A9) & (s | A9) . x = s . x ) by FUNCT_1:48, RELAT_1:61;
hence  y in rng (s | A9) by A19, FUNCT_1:def_3; ::_thesis: verum
end;
then A21: rng (s | A9) = B \ {.c.} by TARSKI:1;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_(g_|_A9)_implies_x_in_dom_(f_*_(s_|_A9))_)_&_(_x_in_dom_(f_*_(s_|_A9))_implies_x_in_dom_(g_|_A9)_)_)
let x be set ; ::_thesis: ( ( x in dom (g | A9) implies x in dom (f * (s | A9)) ) & ( x in dom (f * (s | A9)) implies x in dom (g | A9) ) )
thus  ( x in dom (g | A9) implies x in dom (f * (s | A9)) ) ::_thesis: ( x in dom (f * (s | A9)) implies x in dom (g | A9) )
proof
assume  x in dom (g | A9) ; ::_thesis: x in dom (f * (s | A9))
then A22: x in (dom g) /\ A9 by RELAT_1:61;
then A23: x in A9 by XBOOLE_0:def_4;
A24: x in dom g by A22, XBOOLE_0:def_4;
 x in A9 \/ {.a.} by A23, ZFMISC_1:136;
then  x in (dom g) /\ (A9 \/ {.a.}) by A24, XBOOLE_0:def_4;
then A25: x in dom (f * s) by A8, RELAT_1:61;
then A26: s . x in dom f by FUNCT_1:11;
 x in dom s by A25, FUNCT_1:11;
then  x in (dom s) /\ A9 by A23, XBOOLE_0:def_4;
then A27: x in dom (s | A9) by RELAT_1:61;
then  (s | A9) . x = s . x by FUNCT_1:47;
hence  x in dom (f * (s | A9)) by A26, A27, FUNCT_1:11; ::_thesis: verum
end;
assume A28: x in dom (f * (s | A9)) ; ::_thesis: x in dom (g | A9)
then A29: x in dom (s | A9) by FUNCT_1:11;
then A30: x in (dom s) /\ A9 by RELAT_1:61;
then A31: x in dom s by XBOOLE_0:def_4;
 (s | A9) . x in dom f by A28, FUNCT_1:11;
then  s . x in dom f by A29, FUNCT_1:47;
then  x in dom (g | (A9 \/ {.a.})) by A8, A31, FUNCT_1:11;
then  x in (dom g) /\ (A9 \/ {.a.}) by RELAT_1:61;
then A32: x in dom g by XBOOLE_0:def_4;
 x in A9 by A30, XBOOLE_0:def_4;
then  x in (dom g) /\ A9 by A32, XBOOLE_0:def_4;
hence  x in dom (g | A9) by RELAT_1:61; ::_thesis: verum
end;
then A33: dom (g | A9) = dom (f * (s | A9)) by TARSKI:1;
 a in C9 ;
then  a in dom g by FUNCT_2:def_1;
then  a in (dom g) /\ (A9 \/ {.a.}) by A9, XBOOLE_0:def_4;
then  ( a in dom (f * s) & g . a = (f * s) . a ) by A8, FUNCT_1:48, RELAT_1:61;
then A34: g . a = f . c by FUNCT_1:12;
 (B \ {.c.}) \/ {c} = B \/ {c} by XBOOLE_1:39;
then A35: B = (B \ {.c.}) \/ {c} by A10, ZFMISC_1:40;
A36: dom (s | A9) = A9 by A5, RELAT_1:62, XBOOLE_1:7;
A37: for x being set st x in dom (g | A9) holds
(g | A9) . x = (f * (s | A9)) . x
proof
let x be set ; ::_thesis: ( x in dom (g | A9) implies (g | A9) . x = (f * (s | A9)) . x )
assume  x in dom (g | A9) ; ::_thesis: (g | A9) . x = (f * (s | A9)) . x
then A38: x in (dom g) /\ A9 by RELAT_1:61;
then A39: x in A9 by XBOOLE_0:def_4;
then A40: x in A9 \/ {.a.} by ZFMISC_1:136;
 x in dom g by A38, XBOOLE_0:def_4;
then  x in (dom g) /\ (A9 \/ {.a.}) by A40, XBOOLE_0:def_4;
then  x in dom (f * s) by A8, RELAT_1:61;
then A41: x in dom s by FUNCT_1:11;
then  x in (dom s) /\ A9 by A39, XBOOLE_0:def_4;
then A42: x in dom (s | A9) by RELAT_1:61;
then A43: (s | A9) . x = s . x by FUNCT_1:47;
thus (g | A9) . x = g . x by A39, FUNCT_1:49
.= (f * s) . x by A8, A40, FUNCT_1:49
.= f . (s . x) by A41, FUNCT_1:13
.= (f * (s | A9)) . x by A42, A43, FUNCT_1:13 ; ::_thesis: verum
end;
then A44: g | A9 = f * (s | A9) by A33, FUNCT_1:2;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_g_.:_A9_implies_y_in_f_.:_(B_\_{.c.})_)_&_(_y_in_f_.:_(B_\_{.c.})_implies_y_in_g_.:_A9_)_)
let y be set ; ::_thesis: ( ( y in g .: A9 implies y in f .: (B \ {.c.}) ) & ( y in f .: (B \ {.c.}) implies y in g .: A9 ) )
thus  ( y in g .: A9 implies y in f .: (B \ {.c.}) ) ::_thesis: ( y in f .: (B \ {.c.}) implies y in g .: A9 )
proof
assume  y in g .: A9 ; ::_thesis: y in f .: (B \ {.c.})
then consider x being set  such that
A45: x in dom g and
A46: x in A9 and
A47: y = g . x by FUNCT_1:def_6;
 x in (dom g) /\ A9 by A45, A46, XBOOLE_0:def_4;
then A48: x in dom (g | A9) by RELAT_1:61;
then  x in dom (s | A9) by A33, FUNCT_1:11;
then A49: (s | A9) . x in B \ {.c.} by A21, FUNCT_1:def_3;
 y = (f * (s | A9)) . x by A44, A46, A47, FUNCT_1:49;
then A50: y = f . ((s | A9) . x) by A33, A48, FUNCT_1:12;
 (s | A9) . x in dom f by A33, A48, FUNCT_1:11;
hence  y in f .: (B \ {.c.}) by A50, A49, FUNCT_1:def_6; ::_thesis: verum
end;
assume  y in f .: (B \ {.c.}) ; ::_thesis: y in g .: A9
then consider x being set  such that
 x in dom f and
A51: x in B \ {.c.} and
A52: y = f . x by FUNCT_1:def_6;
set x9 = ((s | A9) ") . x;
A53: ((s | A9) ") . x in A9 by A11, A36, A21, A51, FUNCT_1:32;
 A9 c= C9 by FINSUB_1:def_5;
then  ((s | A9) ") . x in C9 by A53;
then A54: ((s | A9) ") . x in dom g by FUNCT_2:def_1;
 (s | A9) . (((s | A9) ") . x) = x by A11, A21, A51, FUNCT_1:35;
then y = (f * (s | A9)) . (((s | A9) ") . x) by A36, A52, A53, FUNCT_1:13
.= g . (((s | A9) ") . x) by A44, A53, FUNCT_1:49 ;
hence  y in g .: A9 by A53, A54, FUNCT_1:def_6; ::_thesis: verum
end;
then A55: f .: (B \ {.c.}) = g .: A9 by TARSKI:1;
A56: not c in B \ {.c.} by ZFMISC_1:56;
now__::_thesis:_F_$$_((A9_\/_{.a.}),g)_=_F_$$_(B,f)
percases ( A9 = {} or A9 <> {} ) ;
supposeA57: A9 = {} ; ::_thesis: F $$ ((A9 \/ {.a.}),g) = F $$ (B,f)
 B \ {.c.} c= C by FINSUB_1:def_5;
then  B \ {.c.} c= dom f by FUNCT_2:def_1;
then A58: B \ {.c.} = {} by A55, A57;
thus F $$ ((A9 \/ {.a.}),g) = f . c by A1, A34, A57, SETWISEO:17
.= F $$ (B,f) by A1, A35, A58, SETWISEO:17 ; ::_thesis: verum
end;
supposeA59: A9 <> {} ; ::_thesis: F $$ ((A9 \/ {.a.}),g) = F $$ (B,f)
 A9 c= C9 by FINSUB_1:def_5;
then  A9 c= dom g by FUNCT_2:def_1;
then A60: B \ {.c.} <> {} by A55, A59;
thus F $$ ((A9 \/ {.a.}),g) = F . ((F $$ (A9,g)),(g . a)) by A1, A4, A59, Th2
.= F . ((F $$ ((B \ {.c.}),f)),(f . c)) by A3, A34, A11, A36, A21, A33, A37, A59, FUNCT_1:2
.= F $$ (B,f) by A1, A35, A56, A60, Th2 ; ::_thesis: verum
end;
end;
end;
hence  F $$ ((A9 \/ {.a.}),g) = F $$ (B,f) ; ::_thesis: verum
end;
A61: S1[ {}. C9]
proof
assume A62: ( {}. C9 <> {} or F is having_a_unity ) ; ::_thesis: for B being Element of Fin C st ex s being Function st
( dom s = {}. C9 & rng s = B & s is one-to-one & g | ({}. C9) = f * s ) holds
F $$ (({}. C9),g) = F $$ (B,f)
let B be Element of Fin C; ::_thesis: ( ex s being Function st
( dom s = {}. C9 & rng s = B & s is one-to-one & g | ({}. C9) = f * s ) implies F $$ (({}. C9),g) = F $$ (B,f) )
given s being Function such that A63: ( dom s = {}. C9 & rng s = B & s is one-to-one ) and
 g | ({}. C9) = f * s ; ::_thesis: F $$ (({}. C9),g) = F $$ (B,f)
 B, {} are_equipotent by A63, WELLORD2:def_4;
then A64: B = {}. C by CARD_1:26;
 F $$ (({}. C9),g) = the_unity_wrt F by A1, A62, SETWISEO:31;
hence  F $$ (({}. C9),g) = F $$ (B,f) by A1, A62, A64, SETWISEO:31; ::_thesis: verum
end;
 for A being Element of Fin C9 holds S1[A] from SETWISEO:sch_2(A61, A2);
hence  ( ( not A <> {} & not F is having_a_unity ) or for s being Function holds
( not dom s = A or not rng s = B or not s is one-to-one or not g | A = f * s ) or F $$ (A,g) = F $$ (B,f) ) ; ::_thesis: verum
end;

theorem :: SETWOP_2:6
for C, D, E being non empty set
for B being Element of Fin C
for f being Function of C,D
for H being BinOp of E
for h being Function of D,E st H is commutative & H is associative & ( B <> {} or H is having_a_unity ) & f is one-to-one holds
H $$ ((f .: B),h) = H $$ (B,(h * f))
proof
let C, D, E be non empty set ; ::_thesis: for B being Element of Fin C
for f being Function of C,D
for H being BinOp of E
for h being Function of D,E st H is commutative & H is associative & ( B <> {} or H is having_a_unity ) & f is one-to-one holds
H $$ ((f .: B),h) = H $$ (B,(h * f))
let B be Element of Fin C; ::_thesis: for f being Function of C,D
for H being BinOp of E
for h being Function of D,E st H is commutative & H is associative & ( B <> {} or H is having_a_unity ) & f is one-to-one holds
H $$ ((f .: B),h) = H $$ (B,(h * f))
let f be Function of C,D; ::_thesis: for H being BinOp of E
for h being Function of D,E st H is commutative & H is associative & ( B <> {} or H is having_a_unity ) & f is one-to-one holds
H $$ ((f .: B),h) = H $$ (B,(h * f))
let H be BinOp of E; ::_thesis: for h being Function of D,E st H is commutative & H is associative & ( B <> {} or H is having_a_unity ) & f is one-to-one holds
H $$ ((f .: B),h) = H $$ (B,(h * f))
let h be Function of D,E; ::_thesis: ( H is commutative & H is associative & ( B <> {} or H is having_a_unity ) & f is one-to-one implies H $$ ((f .: B),h) = H $$ (B,(h * f)) )
assume that
A1: ( H is commutative & H is associative & ( B <> {} or H is having_a_unity ) ) and
A2: f is one-to-one ; ::_thesis: H $$ ((f .: B),h) = H $$ (B,(h * f))
set s = f | B;
A3: ( rng (f | B) = f .: B & (h * f) | B = h * (f | B) ) by RELAT_1:83, RELAT_1:115;
 B c= C by FINSUB_1:def_5;
then  B c= dom f by FUNCT_2:def_1;
then A4: dom (f | B) = B by RELAT_1:62;
 f | B is one-to-one by A2, FUNCT_1:52;
hence  H $$ ((f .: B),h) = H $$ (B,(h * f)) by A1, A4, A3, Th5; ::_thesis: verum
end;

theorem :: SETWOP_2:7
for C, D being non empty set
for B being Element of Fin C
for F being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & f | B = f9 | B holds
F $$ (B,f) = F $$ (B,f9)
proof
let C, D be non empty set ; ::_thesis: for B being Element of Fin C
for F being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & f | B = f9 | B holds
F $$ (B,f) = F $$ (B,f9)
let B be Element of Fin C; ::_thesis: for F being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & f | B = f9 | B holds
F $$ (B,f) = F $$ (B,f9)
let F be BinOp of D; ::_thesis: for f, f9 being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & f | B = f9 | B holds
F $$ (B,f) = F $$ (B,f9)
let f, f9 be Function of C,D; ::_thesis: ( F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & f | B = f9 | B implies F $$ (B,f) = F $$ (B,f9) )
assume A1: ( F is commutative & F is associative & ( B <> {} or F is having_a_unity ) ) ; ::_thesis: ( not f | B = f9 | B or F $$ (B,f) = F $$ (B,f9) )
set s = id B;
A2: ( dom (id B) = B & rng (id B) = B ) ;
assume  f | B = f9 | B ; ::_thesis: F $$ (B,f) = F $$ (B,f9)
then  f | B = f9 * (id B) by RELAT_1:65;
hence  F $$ (B,f) = F $$ (B,f9) by A1, A2, Th5; ::_thesis: verum
end;

theorem :: SETWOP_2:8
for C, D being non empty set
for B being Element of Fin C
for e being Element of D
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & f .: B = {e} holds
F $$ (B,f) = e
proof
let C, D be non empty set ; ::_thesis: for B being Element of Fin C
for e being Element of D
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & f .: B = {e} holds
F $$ (B,f) = e
let B be Element of Fin C; ::_thesis: for e being Element of D
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & f .: B = {e} holds
F $$ (B,f) = e
let e be Element of D; ::_thesis: for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & f .: B = {e} holds
F $$ (B,f) = e
let F be BinOp of D; ::_thesis: for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & f .: B = {e} holds
F $$ (B,f) = e
let f be Function of C,D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & f .: B = {e} implies F $$ (B,f) = e )
assume that
A1: ( F is commutative & F is associative ) and
A2: F is having_a_unity and
A3: e = the_unity_wrt F ; ::_thesis: ( not f .: B = {e} or F $$ (B,f) = e )
defpred S1[ Element of Fin C] means ( f .: $1 = {e} implies F $$ ($1,f) = e );
A4: for B9 being Element of Fin C
for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
proof
let B9 be Element of Fin C; ::_thesis: for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
let c be Element of C; ::_thesis: ( S1[B9] & not c in B9 implies S1[B9 \/ {.c.}] )
assume that
A5: ( f .: B9 = {e} implies F $$ (B9,f) = e ) and
A6: not c in B9 and
A7: f .: (B9 \/ {c}) = {e} ; ::_thesis: F $$ ((B9 \/ {.c.}),f) = e
A8: now__::_thesis:_F_$$_((B9_\/_{.c.}),f)_=_F_._(e,(f_._c))
percases ( B9 = {} or B9 <> {} ) ;
suppose B9 = {} ; ::_thesis: F $$ ((B9 \/ {.c.}),f) = F . (e,(f . c))
then A9: B9 = {}. C ;
thus F $$ ((B9 \/ {.c.}),f) = F . ((F $$ (B9,f)),(f . c)) by A1, A2, A6, Th2
.= F . (e,(f . c)) by A1, A2, A3, A9, SETWISEO:31 ; ::_thesis: verum
end;
supposeA10: B9 <> {} ; ::_thesis: F $$ ((B9 \/ {.c.}),f) = F . (e,(f . c))
 B9 c= C by FINSUB_1:def_5;
then A11: B9 c= dom f by FUNCT_2:def_1;
 f .: B9 c= {e} by A7, RELAT_1:123, XBOOLE_1:7;
hence  F $$ ((B9 \/ {.c.}),f) = F . (e,(f . c)) by A1, A5, A6, A10, A11, Th2, ZFMISC_1:33; ::_thesis: verum
end;
end;
end;
 {.c.} c= C by FINSUB_1:def_5;
then A12: {c} c= dom f by FUNCT_2:def_1;
then A13: c in dom f by ZFMISC_1:31;
 Im (f,c) c= {e} by A7, RELAT_1:123, XBOOLE_1:7;
then  Im (f,c) = {e} by A12, ZFMISC_1:33;
then  {e} = {(f . c)} by A13, FUNCT_1:59;
then  f . c = e by ZFMISC_1:3;
hence  F $$ ((B9 \/ {.c.}),f) = e by A2, A3, A8, SETWISEO:15; ::_thesis: verum
end;
A14: S1[ {}. C] ;
 for B being Element of Fin C holds S1[B] from SETWISEO:sch_2(A14, A4);
hence  ( not f .: B = {e} or F $$ (B,f) = e ) ; ::_thesis: verum
end;

theorem Th9: :: SETWOP_2:9
for C, D being non empty set
for B being Element of Fin C
for e being Element of D
for F, G being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds
G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))
proof
let C, D be non empty set ; ::_thesis: for B being Element of Fin C
for e being Element of D
for F, G being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds
G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))
let B be Element of Fin C; ::_thesis: for e being Element of D
for F, G being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds
G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))
let e be Element of D; ::_thesis: for F, G being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds
G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))
let F, G be BinOp of D; ::_thesis: for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds
G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))
let f, f9 be Function of C,D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) implies G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: e = the_unity_wrt F and
A3: G . (e,e) = e and
A4: for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ; ::_thesis: G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))
defpred S1[ Element of Fin C] means G . ((F $$ ($1,f)),(F $$ ($1,f9))) = F $$ ($1,(G .: (f,f9)));
A5: for B9 being Element of Fin C
for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
proof
let B be Element of Fin C; ::_thesis: for b being Element of C st S1[B] & not b in B holds
S1[B \/ {.b.}]
let c be Element of C; ::_thesis: ( S1[B] & not c in B implies S1[B \/ {.c.}] )
assume that
A6: G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) and
A7: not c in B ; ::_thesis: S1[B \/ {.c.}]
set s9 = F $$ (B,f9);
set s = F $$ (B,f);
 ( F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c)) & F $$ ((B \/ {.c.}),f9) = F . ((F $$ (B,f9)),(f9 . c)) ) by A1, A7, Th2;
hence G . ((F $$ ((B \/ {.c.}),f)),(F $$ ((B \/ {.c.}),f9))) = F . ((G . ((F $$ (B,f)),(F $$ (B,f9)))),(G . ((f . c),(f9 . c)))) by A4
.= F . ((G . ((F $$ (B,f)),(F $$ (B,f9)))),((G .: (f,f9)) . c)) by FUNCOP_1:37
.= F $$ ((B \/ {.c.}),(G .: (f,f9))) by A1, A6, A7, Th2 ;
::_thesis: verum
end;
 ( F $$ (({}. C),f) = e & F $$ (({}. C),f9) = e ) by A1, A2, SETWISEO:31;
then A8: S1[ {}. C] by A1, A2, A3, SETWISEO:31;
 for B being Element of Fin C holds S1[B] from SETWISEO:sch_2(A8, A5);
hence  G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) ; ::_thesis: verum
end;

Lm3:  for D being non empty set
for F being BinOp of D st F is commutative & F is associative holds
for d1, d2, d3, d4 being Element of D holds F . ((F . (d1,d2)),(F . (d3,d4))) = F . ((F . (d1,d3)),(F . (d2,d4)))
proof
let D be non empty set ; ::_thesis: for F being BinOp of D st F is commutative & F is associative holds
for d1, d2, d3, d4 being Element of D holds F . ((F . (d1,d2)),(F . (d3,d4))) = F . ((F . (d1,d3)),(F . (d2,d4)))
let F be BinOp of D; ::_thesis: ( F is commutative & F is associative implies for d1, d2, d3, d4 being Element of D holds F . ((F . (d1,d2)),(F . (d3,d4))) = F . ((F . (d1,d3)),(F . (d2,d4))) )
assume that
A1: F is commutative and
A2: F is associative ; ::_thesis: for d1, d2, d3, d4 being Element of D holds F . ((F . (d1,d2)),(F . (d3,d4))) = F . ((F . (d1,d3)),(F . (d2,d4)))
let d1, d2, d3, d4 be Element of D; ::_thesis: F . ((F . (d1,d2)),(F . (d3,d4))) = F . ((F . (d1,d3)),(F . (d2,d4)))
thus F . ((F . (d1,d2)),(F . (d3,d4))) = F . (d1,(F . (d2,(F . (d3,d4))))) by A2, BINOP_1:def_3
.= F . (d1,(F . ((F . (d2,d3)),d4))) by A2, BINOP_1:def_3
.= F . (d1,(F . ((F . (d3,d2)),d4))) by A1, BINOP_1:def_2
.= F . (d1,(F . (d3,(F . (d2,d4))))) by A2, BINOP_1:def_3
.= F . ((F . (d1,d3)),(F . (d2,d4))) by A2, BINOP_1:def_3 ; ::_thesis: verum
end;

theorem :: SETWOP_2:10
for C, D being non empty set
for B being Element of Fin C
for F being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity holds
F . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(F .: (f,f9)))
proof
let C, D be non empty set ; ::_thesis: for B being Element of Fin C
for F being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity holds
F . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(F .: (f,f9)))
let B be Element of Fin C; ::_thesis: for F being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity holds
F . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(F .: (f,f9)))
let F be BinOp of D; ::_thesis: for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity holds
F . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(F .: (f,f9)))
let f, f9 be Function of C,D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity implies F . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(F .: (f,f9))) )
set e = the_unity_wrt F;
assume A1: ( F is commutative & F is associative & F is having_a_unity ) ; ::_thesis: F . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(F .: (f,f9)))
then  ( F . ((the_unity_wrt F),(the_unity_wrt F)) = the_unity_wrt F & ( for d1, d2, d3, d4 being Element of D holds F . ((F . (d1,d2)),(F . (d3,d4))) = F . ((F . (d1,d3)),(F . (d2,d4))) ) ) by Lm3, SETWISEO:15;
hence  F . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(F .: (f,f9))) by A1, Th9; ::_thesis: verum
end;

theorem :: SETWOP_2:11
for C, D being non empty set
for B being Element of Fin C
for F, G being BinOp of D
for f, f9 being Function of C,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
G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))
proof
let C, D be non empty set ; ::_thesis: for B being Element of Fin C
for F, G being BinOp of D
for f, f9 being Function of C,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
G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))
let B be Element of Fin C; ::_thesis: for F, G being BinOp of D
for f, f9 being Function of C,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
G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))
let F, G be BinOp of D; ::_thesis: for f, f9 being Function of C,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
G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))
let f, f9 be Function of C,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 G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: ( F is having_an_inverseOp & G = F * ((id D),(the_inverseOp_wrt F)) ) ; ::_thesis: G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))
set e = the_unity_wrt F;
 ( G . ((the_unity_wrt F),(the_unity_wrt F)) = the_unity_wrt F & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) ) by A1, A2, FINSEQOP:86, FINSEQOP:89;
hence  G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) by A1, Th9; ::_thesis: verum
end;

theorem Th12: :: SETWOP_2:12
for C, D being non empty set
for B being Element of Fin C
for e, d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (d,e) = e holds
G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
proof
let C, D be non empty set ; ::_thesis: for B being Element of Fin C
for e, d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (d,e) = e holds
G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
let B be Element of Fin C; ::_thesis: for e, d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (d,e) = e holds
G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
let e, d be Element of D; ::_thesis: for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (d,e) = e holds
G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
let F, G be BinOp of D; ::_thesis: for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (d,e) = e holds
G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
let f be Function of C,D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (d,e) = e implies G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: e = the_unity_wrt F and
A3: G is_distributive_wrt F ; ::_thesis: ( not G . (d,e) = e or G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) )
defpred S1[ Element of Fin C] means G . (d,(F $$ ($1,f))) = F $$ ($1,(G [;] (d,f)));
A4: for B9 being Element of Fin C
for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
proof
let B9 be Element of Fin C; ::_thesis: for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
let c be Element of C; ::_thesis: ( S1[B9] & not c in B9 implies S1[B9 \/ {.c.}] )
assume that
A5: G . (d,(F $$ (B9,f))) = F $$ (B9,(G [;] (d,f))) and
A6: not c in B9 ; ::_thesis: S1[B9 \/ {.c.}]
thus G . (d,(F $$ ((B9 \/ {.c.}),f))) = G . (d,(F . ((F $$ (B9,f)),(f . c)))) by A1, A6, Th2
.= F . ((G . (d,(F $$ (B9,f)))),(G . (d,(f . c)))) by A3, BINOP_1:11
.= F . ((F $$ (B9,(G [;] (d,f)))),((G [;] (d,f)) . c)) by A5, FUNCOP_1:53
.= F $$ ((B9 \/ {.c.}),(G [;] (d,f))) by A1, A6, Th2 ; ::_thesis: verum
end;
assume  G . (d,e) = e ; ::_thesis: G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
then G . (d,(F $$ (({}. C),f))) = e by A1, A2, SETWISEO:31
.= F $$ (({}. C),(G [;] (d,f))) by A1, A2, SETWISEO:31 ;
then A7: S1[ {}. C] ;
 for B being Element of Fin C holds S1[B] from SETWISEO:sch_2(A7, A4);
hence  G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) ; ::_thesis: verum
end;

theorem Th13: :: SETWOP_2:13
for C, D being non empty set
for B being Element of Fin C
for e, d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
proof
let C, D be non empty set ; ::_thesis: for B being Element of Fin C
for e, d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
let B be Element of Fin C; ::_thesis: for e, d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
let e, d be Element of D; ::_thesis: for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
let F, G be BinOp of D; ::_thesis: for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
let f be Function of C,D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e implies G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d))) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: e = the_unity_wrt F and
A3: G is_distributive_wrt F ; ::_thesis: ( not G . (e,d) = e or G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d))) )
defpred S1[ Element of Fin C] means G . ((F $$ ($1,f)),d) = F $$ ($1,(G [:] (f,d)));
A4: for B9 being Element of Fin C
for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
proof
let B9 be Element of Fin C; ::_thesis: for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
let c be Element of C; ::_thesis: ( S1[B9] & not c in B9 implies S1[B9 \/ {.c.}] )
assume that
A5: G . ((F $$ (B9,f)),d) = F $$ (B9,(G [:] (f,d))) and
A6: not c in B9 ; ::_thesis: S1[B9 \/ {.c.}]
thus G . ((F $$ ((B9 \/ {.c.}),f)),d) = G . ((F . ((F $$ (B9,f)),(f . c))),d) by A1, A6, Th2
.= F . ((G . ((F $$ (B9,f)),d)),(G . ((f . c),d))) by A3, BINOP_1:11
.= F . ((F $$ (B9,(G [:] (f,d)))),((G [:] (f,d)) . c)) by A5, FUNCOP_1:48
.= F $$ ((B9 \/ {.c.}),(G [:] (f,d))) by A1, A6, Th2 ; ::_thesis: verum
end;
assume  G . (e,d) = e ; ::_thesis: G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
then G . ((F $$ (({}. C),f)),d) = e by A1, A2, SETWISEO:31
.= F $$ (({}. C),(G [:] (f,d))) by A1, A2, SETWISEO:31 ;
then A7: S1[ {}. C] ;
 for B being Element of Fin C holds S1[B] from SETWISEO:sch_2(A7, A4);
hence  G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d))) ; ::_thesis: verum
end;

theorem :: SETWOP_2:14
for C, D being non empty set
for B being Element of Fin C
for d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
proof
let C, D be non empty set ; ::_thesis: for B being Element of Fin C
for d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
let B be Element of Fin C; ::_thesis: for d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
let d be Element of D; ::_thesis: for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
let F, G be BinOp of D; ::_thesis: for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
let f be Function of C,D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: F is having_an_inverseOp and
A3: G is_distributive_wrt F ; ::_thesis: G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
set e = the_unity_wrt F;
 G . (d,(the_unity_wrt F)) = the_unity_wrt F by A1, A2, A3, FINSEQOP:66;
hence  G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) by A1, A3, Th12; ::_thesis: verum
end;

theorem :: SETWOP_2:15
for C, D being non empty set
for B being Element of Fin C
for d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
proof
let C, D be non empty set ; ::_thesis: for B being Element of Fin C
for d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
let B be Element of Fin C; ::_thesis: for d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
let d be Element of D; ::_thesis: for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
let F, G be BinOp of D; ::_thesis: for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
let f be Function of C,D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d))) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: F is having_an_inverseOp and
A3: G is_distributive_wrt F ; ::_thesis: G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
set e = the_unity_wrt F;
 G . ((the_unity_wrt F),d) = the_unity_wrt F by A1, A2, A3, FINSEQOP:66;
hence  G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d))) by A1, A3, Th13; ::_thesis: verum
end;

theorem Th16: :: SETWOP_2:16
for C, E, D being non empty set
for B being Element of Fin C
for F being BinOp of D
for f being Function of C,D
for H being BinOp of E
for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h . (F $$ (B,f)) = H $$ (B,(h * f))
proof
let C, E, D be non empty set ; ::_thesis: for B being Element of Fin C
for F being BinOp of D
for f being Function of C,D
for H being BinOp of E
for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h . (F $$ (B,f)) = H $$ (B,(h * f))
let B be Element of Fin C; ::_thesis: for F being BinOp of D
for f being Function of C,D
for H being BinOp of E
for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h . (F $$ (B,f)) = H $$ (B,(h * f))
let F be BinOp of D; ::_thesis: for f being Function of C,D
for H being BinOp of E
for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h . (F $$ (B,f)) = H $$ (B,(h * f))
let f be Function of C,D; ::_thesis: for H being BinOp of E
for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h . (F $$ (B,f)) = H $$ (B,(h * f))
let H be BinOp of E; ::_thesis: for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h . (F $$ (B,f)) = H $$ (B,(h * f))
let h be Function of D,E; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h . (F $$ (B,f)) = H $$ (B,(h * f)) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: ( H is commutative & H is associative & H is having_a_unity ) and
A3: h . (the_unity_wrt F) = the_unity_wrt H and
A4: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h . (F $$ (B,f)) = H $$ (B,(h * f))
defpred S1[ Element of Fin C] means h . (F $$ ($1,f)) = H $$ ($1,(h * f));
A5: for B9 being Element of Fin C
for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
proof
let B be Element of Fin C; ::_thesis: for b being Element of C st S1[B] & not b in B holds
S1[B \/ {.b.}]
let c be Element of C; ::_thesis: ( S1[B] & not c in B implies S1[B \/ {.c.}] )
assume that
A6: h . (F $$ (B,f)) = H $$ (B,(h * f)) and
A7: not c in B ; ::_thesis: S1[B \/ {.c.}]
thus h . (F $$ ((B \/ {.c.}),f)) = h . (F . ((F $$ (B,f)),(f . c))) by A1, A7, Th2
.= H . ((H $$ (B,(h * f))),(h . (f . c))) by A4, A6
.= H . ((H $$ (B,(h * f))),((h * f) . c)) by FUNCT_2:15
.= H $$ ((B \/ {.c.}),(h * f)) by A2, A7, Th2 ; ::_thesis: verum
end;
h . (F $$ (({}. C),f)) = the_unity_wrt H by A1, A3, SETWISEO:31
.= H $$ (({}. C),(h * f)) by A2, SETWISEO:31 ;
then A8: S1[ {}. C] ;
 for B being Element of Fin C holds S1[B] from SETWISEO:sch_2(A8, A5);
hence  h . (F $$ (B,f)) = H $$ (B,(h * f)) ; ::_thesis: verum
end;

theorem :: SETWOP_2:17
for C, D being non empty set
for B being Element of Fin C
for F being BinOp of D
for u being UnOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F holds
u . (F $$ (B,f)) = F $$ (B,(u * f))
proof
let C, D be non empty set ; ::_thesis: for B being Element of Fin C
for F being BinOp of D
for u being UnOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F holds
u . (F $$ (B,f)) = F $$ (B,(u * f))
let B be Element of Fin C; ::_thesis: for F being BinOp of D
for u being UnOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F holds
u . (F $$ (B,f)) = F $$ (B,(u * f))
let F be BinOp of D; ::_thesis: for u being UnOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F holds
u . (F $$ (B,f)) = F $$ (B,(u * f))
let u be UnOp of D; ::_thesis: for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F holds
u . (F $$ (B,f)) = F $$ (B,(u * f))
let f be Function of C,D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F implies u . (F $$ (B,f)) = F $$ (B,(u * f)) )
assume A1: ( F is commutative & F is associative & F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F ) ; ::_thesis: ( not u is_distributive_wrt F or u . (F $$ (B,f)) = F $$ (B,(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 $$ (B,f)) = F $$ (B,(u * f))
hence  u . (F $$ (B,f)) = F $$ (B,(u * f)) by A1, Th16; ::_thesis: verum
end;

theorem :: SETWOP_2:18
for C, D being non empty set
for B being Element of Fin C
for d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
(G [;] (d,(id D))) . (F $$ (B,f)) = F $$ (B,((G [;] (d,(id D))) * f))
proof
let C, D be non empty set ; ::_thesis: for B being Element of Fin C
for d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
(G [;] (d,(id D))) . (F $$ (B,f)) = F $$ (B,((G [;] (d,(id D))) * f))
let B be Element of Fin C; ::_thesis: for d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
(G [;] (d,(id D))) . (F $$ (B,f)) = F $$ (B,((G [;] (d,(id D))) * f))
let d be Element of D; ::_thesis: for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
(G [;] (d,(id D))) . (F $$ (B,f)) = F $$ (B,((G [;] (d,(id D))) * f))
let F, G be BinOp of D; ::_thesis: for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
(G [;] (d,(id D))) . (F $$ (B,f)) = F $$ (B,((G [;] (d,(id D))) * f))
let f be Function of C,D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies (G [;] (d,(id D))) . (F $$ (B,f)) = F $$ (B,((G [;] (d,(id D))) * f)) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: F is having_an_inverseOp and
A3: G is_distributive_wrt F ; ::_thesis: (G [;] (d,(id D))) . (F $$ (B,f)) = F $$ (B,((G [;] (d,(id D))) * f))
set e = the_unity_wrt F;
set u = G [;] (d,(id D));
 G [;] (d,(id D)) is_distributive_wrt F by A3, FINSEQOP:54;
then A4: for d1, d2 being Element of D holds (G [;] (d,(id D))) . (F . (d1,d2)) = F . (((G [;] (d,(id D))) . d1),((G [;] (d,(id D))) . d2)) by BINOP_1:def_12;
 (G [;] (d,(id D))) . (the_unity_wrt F) = the_unity_wrt F by A1, A2, A3, FINSEQOP:69;
hence  (G [;] (d,(id D))) . (F $$ (B,f)) = F $$ (B,((G [;] (d,(id D))) * f)) by A1, A4, Th16; ::_thesis: verum
end;

theorem :: SETWOP_2:19
for C, D being non empty set
for B being Element of Fin C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp holds
(the_inverseOp_wrt F) . (F $$ (B,f)) = F $$ (B,((the_inverseOp_wrt F) * f))
proof
let C, D be non empty set ; ::_thesis: for B being Element of Fin C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp holds
(the_inverseOp_wrt F) . (F $$ (B,f)) = F $$ (B,((the_inverseOp_wrt F) * f))
let B be Element of Fin C; ::_thesis: for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp holds
(the_inverseOp_wrt F) . (F $$ (B,f)) = F $$ (B,((the_inverseOp_wrt F) * f))
let F be BinOp of D; ::_thesis: for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp holds
(the_inverseOp_wrt F) . (F $$ (B,f)) = F $$ (B,((the_inverseOp_wrt F) * f))
let f be Function of C,D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp implies (the_inverseOp_wrt F) . (F $$ (B,f)) = F $$ (B,((the_inverseOp_wrt F) * f)) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: F is having_an_inverseOp ; ::_thesis: (the_inverseOp_wrt F) . (F $$ (B,f)) = F $$ (B,((the_inverseOp_wrt F) * f))
set e = the_unity_wrt F;
set u = the_inverseOp_wrt F;
 the_inverseOp_wrt F is_distributive_wrt F by A1, A2, FINSEQOP:63;
then A3: for d1, d2 being Element of D holds (the_inverseOp_wrt F) . (F . (d1,d2)) = F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . d2)) by BINOP_1:def_12;
 (the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F by A1, A2, FINSEQOP:61;
hence  (the_inverseOp_wrt F) . (F $$ (B,f)) = F $$ (B,((the_inverseOp_wrt F) * f)) by A1, A3, Th16; ::_thesis: verum
end;

definition
let D be non empty set ;
let p be FinSequence of D;
let d be Element of D;
func [#] (p,d) ->  Function of NAT,D equals :: SETWOP_2:def 1
(NAT --> d) +* p;
coherence
 (NAT --> d) +* p is Function of NAT,D ;
end;

:: deftheorem  defines [#] SETWOP_2:def_1_:_
 for D being non empty set
for p being FinSequence of D
for d being Element of D holds [#] (p,d) = (NAT --> d) +* p;

theorem Th20: :: SETWOP_2:20
for D being non empty set
for d being Element of D
for i being Nat
for p being FinSequence of D holds
( ( i in dom p implies ([#] (p,d)) . i = p . i ) & ( not i in dom p implies ([#] (p,d)) . i = d ) )
proof
let D be non empty set ; ::_thesis: for d being Element of D
for i being Nat
for p being FinSequence of D holds
( ( i in dom p implies ([#] (p,d)) . i = p . i ) & ( not i in dom p implies ([#] (p,d)) . i = d ) )
let d be Element of D; ::_thesis: for i being Nat
for p being FinSequence of D holds
( ( i in dom p implies ([#] (p,d)) . i = p . i ) & ( not i in dom p implies ([#] (p,d)) . i = d ) )
let i be Nat; ::_thesis: for p being FinSequence of D holds
( ( i in dom p implies ([#] (p,d)) . i = p . i ) & ( not i in dom p implies ([#] (p,d)) . i = d ) )
let p be FinSequence of D; ::_thesis: ( ( i in dom p implies ([#] (p,d)) . i = p . i ) & ( not i in dom p implies ([#] (p,d)) . i = d ) )
thus  ( i in dom p implies ([#] (p,d)) . i = p . i ) by FUNCT_4:13; ::_thesis: ( not i in dom p implies ([#] (p,d)) . i = d )
A1: i in NAT by ORDINAL1:def_12;
assume  not i in dom p ; ::_thesis: ([#] (p,d)) . i = d
hence ([#] (p,d)) . i = (NAT --> d) . i by FUNCT_4:11
.= d by A1, FUNCOP_1:7 ;
::_thesis: verum
end;

theorem :: SETWOP_2:21
for D being non empty set
for d being Element of D
for p being FinSequence of D holds ([#] (p,d)) | (dom p) = p
proof
let D be non empty set ; ::_thesis: for d being Element of D
for p being FinSequence of D holds ([#] (p,d)) | (dom p) = p
let d be Element of D; ::_thesis: for p being FinSequence of D holds ([#] (p,d)) | (dom p) = p
let p be FinSequence of D; ::_thesis: ([#] (p,d)) | (dom p) = p
set k = len p;
set f = [#] (p,d);
 Seg (len p) c= NAT ;
then  Seg (len p) c= dom ([#] (p,d)) by FUNCT_2:def_1;
then A1: dom (([#] (p,d)) | (Seg (len p))) = Seg (len p) by RELAT_1:62;
A2: dom p = Seg (len p) by FINSEQ_1:def_3;
now__::_thesis:_for_x_being_set_st_x_in_Seg_(len_p)_holds_
(([#]_(p,d))_|_(Seg_(len_p)))_._x_=_p_._x
let x be set ; ::_thesis: ( x in Seg (len p) implies (([#] (p,d)) | (Seg (len p))) . x = p . x )
assume A3: x in Seg (len p) ; ::_thesis: (([#] (p,d)) | (Seg (len p))) . x = p . x
then  (([#] (p,d)) | (Seg (len p))) . x = ([#] (p,d)) . x by A1, FUNCT_1:47;
hence  (([#] (p,d)) | (Seg (len p))) . x = p . x by A2, A3, Th20; ::_thesis: verum
end;
hence  ([#] (p,d)) | (dom p) = p by A1, A2, FUNCT_1:2; ::_thesis: verum
end;

theorem :: SETWOP_2:22
for D being non empty set
for d being Element of D
for p, q being FinSequence of D holds ([#] ((p ^ q),d)) | (dom p) = p
proof
let D be non empty set ; ::_thesis: for d being Element of D
for p, q being FinSequence of D holds ([#] ((p ^ q),d)) | (dom p) = p
let d be Element of D; ::_thesis: for p, q being FinSequence of D holds ([#] ((p ^ q),d)) | (dom p) = p
let p, q be FinSequence of D; ::_thesis: ([#] ((p ^ q),d)) | (dom p) = p
set k = len p;
set f = [#] ((p ^ q),d);
 Seg (len p) c= NAT ;
then  Seg (len p) c= dom ([#] ((p ^ q),d)) by FUNCT_2:def_1;
then A1: dom (([#] ((p ^ q),d)) | (Seg (len p))) = Seg (len p) by RELAT_1:62;
A2: dom p = Seg (len p) by FINSEQ_1:def_3;
now__::_thesis:_for_x_being_set_st_x_in_Seg_(len_p)_holds_
(([#]_((p_^_q),d))_|_(Seg_(len_p)))_._x_=_p_._x
let x be set ; ::_thesis: ( x in Seg (len p) implies (([#] ((p ^ q),d)) | (Seg (len p))) . x = p . x )
 len p <= (len p) + (len q) by NAT_1:12;
then  len p <= len (p ^ q) by FINSEQ_1:22;
then A3: ( Seg (len (p ^ q)) = dom (p ^ q) & Seg (len p) c= Seg (len (p ^ q)) ) by FINSEQ_1:5, FINSEQ_1:def_3;
assume A4: x in Seg (len p) ; ::_thesis: (([#] ((p ^ q),d)) | (Seg (len p))) . x = p . x
then  (([#] ((p ^ q),d)) | (Seg (len p))) . x = ([#] ((p ^ q),d)) . x by A1, FUNCT_1:47;
hence (([#] ((p ^ q),d)) | (Seg (len p))) . x = (p ^ q) . x by A4, A3, Th20
.= p . x by A2, A4, FINSEQ_1:def_7 ;
::_thesis: verum
end;
hence  ([#] ((p ^ q),d)) | (dom p) = p by A1, A2, FUNCT_1:2; ::_thesis: verum
end;

theorem :: SETWOP_2:23
for D being non empty set
for d being Element of D
for p being FinSequence of D holds rng ([#] (p,d)) = (rng p) \/ {d}
proof
let D be non empty set ; ::_thesis: for d being Element of D
for p being FinSequence of D holds rng ([#] (p,d)) = (rng p) \/ {d}
let d be Element of D; ::_thesis: for p being FinSequence of D holds rng ([#] (p,d)) = (rng p) \/ {d}
let p be FinSequence of D; ::_thesis: rng ([#] (p,d)) = (rng p) \/ {d}
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_rng_([#]_(p,d))_implies_y_in_(rng_p)_\/_{d}_)_&_(_y_in_(rng_p)_\/_{d}_implies_y_in_rng_([#]_(p,d))_)_)
let y be set ; ::_thesis: ( ( y in rng ([#] (p,d)) implies y in (rng p) \/ {d} ) & ( y in (rng p) \/ {d} implies y in rng ([#] (p,d)) ) )
thus  ( y in rng ([#] (p,d)) implies y in (rng p) \/ {d} ) ::_thesis: ( y in (rng p) \/ {d} implies y in rng ([#] (p,d)) )
proof
assume  y in rng ([#] (p,d)) ; ::_thesis: y in (rng p) \/ {d}
then consider x being set  such that
A1: x in dom ([#] (p,d)) and
A2: y = ([#] (p,d)) . x by FUNCT_1:def_3;
reconsider i = x as Element of NAT by A1;
now__::_thesis:_(_(_i_in_dom_p_&_y_in_rng_p_)_or_(_not_i_in_dom_p_&_y_in_{d}_)_)
percases ( i in dom p or not i in dom p ) ;
caseA3: i in dom p ; ::_thesis: y in rng p
then  y = p . i by A2, Th20;
hence  y in rng p by A3, FUNCT_1:def_3; ::_thesis: verum
end;
case not i in dom p ; ::_thesis: y in {d}
then  y = d by A2, Th20;
hence  y in {d} by TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  y in (rng p) \/ {d} by XBOOLE_0:def_3; ::_thesis: verum
end;
assume A4: y in (rng p) \/ {d} ; ::_thesis: y in rng ([#] (p,d))
now__::_thesis:_y_in_rng_([#]_(p,d))
percases ( y in rng p or y in {d} ) by A4, XBOOLE_0:def_3;
suppose y in rng p ; ::_thesis: y in rng ([#] (p,d))
then consider i being Nat such that
A5: i in dom p and
A6: y = p . i by FINSEQ_2:10;
 y = ([#] (p,d)) . i by A5, A6, Th20;
hence  y in rng ([#] (p,d)) by A5, FUNCT_2:4; ::_thesis: verum
end;
supposeA7: y in {d} ; ::_thesis: y in rng ([#] (p,d))
 dom p = Seg (len p) by FINSEQ_1:def_3;
then A8: not (len p) + 1 in dom p by Lm2;
 y = d by A7, TARSKI:def_1;
then  y = ([#] (p,d)) . ((len p) + 1) by A8, Th20;
hence  y in rng ([#] (p,d)) by FUNCT_2:4; ::_thesis: verum
end;
end;
end;
hence  y in rng ([#] (p,d)) ; ::_thesis: verum
end;
hence  rng ([#] (p,d)) = (rng p) \/ {d} by TARSKI:1; ::_thesis: verum
end;

theorem :: SETWOP_2:24
for E, D being non empty set
for d being Element of D
for h being Function of D,E
for p being FinSequence of D holds h * ([#] (p,d)) = [#] ((h * p),(h . d))
proof
let E, D be non empty set ; ::_thesis: for d being Element of D
for h being Function of D,E
for p being FinSequence of D holds h * ([#] (p,d)) = [#] ((h * p),(h . d))
let d be Element of D; ::_thesis: for h being Function of D,E
for p being FinSequence of D holds h * ([#] (p,d)) = [#] ((h * p),(h . d))
let h be Function of D,E; ::_thesis: for p being FinSequence of D holds h * ([#] (p,d)) = [#] ((h * p),(h . d))
let p be FinSequence of D; ::_thesis: h * ([#] (p,d)) = [#] ((h * p),(h . d))
now__::_thesis:_for_i_being_Element_of_NAT_holds_(h_*_([#]_(p,d)))_._i_=_([#]_((h_*_p),(h_._d)))_._i
let i be Element of NAT ; ::_thesis: (h * ([#] (p,d))) . i = ([#] ((h * p),(h . d))) . i
A1: dom (h * p) = Seg (len (h * p)) by FINSEQ_1:def_3;
A2: ( len (h * p) = len p & Seg (len p) = dom p ) by FINSEQ_1:def_3, FINSEQ_2:33;
now__::_thesis:_h_._(([#]_(p,d))_._i)_=_([#]_((h_*_p),(h_._d)))_._i
percases ( i in dom p or not i in dom p ) ;
supposeA3: i in dom p ; ::_thesis: h . (([#] (p,d)) . i) = ([#] ((h * p),(h . d))) . i
hence h . (([#] (p,d)) . i) = h . (p . i) by Th20
.= (h * p) . i by A3, FUNCT_1:13
.= ([#] ((h * p),(h . d))) . i by A2, A1, A3, Th20 ;
::_thesis: verum
end;
supposeA4: not i in dom p ; ::_thesis: h . (([#] (p,d)) . i) = ([#] ((h * p),(h . d))) . i
hence h . (([#] (p,d)) . i) = h . d by Th20
.= ([#] ((h * p),(h . d))) . i by A2, A1, A4, Th20 ;
::_thesis: verum
end;
end;
end;
hence  (h * ([#] (p,d))) . i = ([#] ((h * p),(h . d))) . i by FUNCT_2:15; ::_thesis: verum
end;
hence  h * ([#] (p,d)) = [#] ((h * p),(h . d)) by FUNCT_2:63; ::_thesis: verum
end;

Lm4:  for D being non empty set
for e being Element of D
for F being BinOp of D
for p, q being FinSequence of D st len p = len q & F . (e,e) = e holds
F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e)
proof
let D be non empty set ; ::_thesis: for e being Element of D
for F being BinOp of D
for p, q being FinSequence of D st len p = len q & F . (e,e) = e holds
F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e)
let e be Element of D; ::_thesis: for F being BinOp of D
for p, q being FinSequence of D st len p = len q & F . (e,e) = e holds
F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e)
let F be BinOp of D; ::_thesis: for p, q being FinSequence of D st len p = len q & F . (e,e) = e holds
F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e)
let p, q be FinSequence of D; ::_thesis: ( len p = len q & F . (e,e) = e implies F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e) )
assume that
A1: len p = len q and
A2: F . (e,e) = e ; ::_thesis: F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e)
set r = F .: (p,q);
A3: len (F .: (p,q)) = len p by A1, FINSEQ_2:72;
A4: dom (F .: (p,q)) = Seg (len (F .: (p,q))) by FINSEQ_1:def_3;
A5: dom p = Seg (len p) by FINSEQ_1:def_3;
A6: dom q = Seg (len q) by FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Element_of_NAT_holds_(F_.:_(([#]_(p,e)),([#]_(q,e))))_._i_=_([#]_((F_.:_(p,q)),e))_._i
let i be Element of NAT ; ::_thesis: (F .: (([#] (p,e)),([#] (q,e)))) . i = ([#] ((F .: (p,q)),e)) . i
now__::_thesis:_F_._((([#]_(p,e))_._i),(([#]_(q,e))_._i))_=_([#]_((F_.:_(p,q)),e))_._i
percases ( i in dom p or not i in dom p ) ;
supposeA7: i in dom p ; ::_thesis: F . ((([#] (p,e)) . i),(([#] (q,e)) . i)) = ([#] ((F .: (p,q)),e)) . i
hence F . ((([#] (p,e)) . i),(([#] (q,e)) . i)) = F . ((p . i),(([#] (q,e)) . i)) by Th20
.= F . ((p . i),(q . i)) by A1, A5, A6, A7, Th20
.= (F .: (p,q)) . i by A3, A5, A4, A7, FUNCOP_1:22
.= ([#] ((F .: (p,q)),e)) . i by A3, A5, A4, A7, Th20 ;
::_thesis: verum
end;
supposeA8: not i in dom p ; ::_thesis: F . ((([#] (p,e)) . i),(([#] (q,e)) . i)) = ([#] ((F .: (p,q)),e)) . i
hence F . ((([#] (p,e)) . i),(([#] (q,e)) . i)) = F . (e,(([#] (q,e)) . i)) by Th20
.= e by A1, A2, A5, A6, A8, Th20
.= ([#] ((F .: (p,q)),e)) . i by A3, A5, A4, A8, Th20 ;
::_thesis: verum
end;
end;
end;
hence  (F .: (([#] (p,e)),([#] (q,e)))) . i = ([#] ((F .: (p,q)),e)) . i by FUNCOP_1:37; ::_thesis: verum
end;
hence  F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e) by FUNCT_2:63; ::_thesis: verum
end;

Lm5:  for D being non empty set
for e, d being Element of D
for F being BinOp of D
for p being FinSequence of D st F . (e,d) = e holds
F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)
proof
let D be non empty set ; ::_thesis: for e, d being Element of D
for F being BinOp of D
for p being FinSequence of D st F . (e,d) = e holds
F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)
let e, d be Element of D; ::_thesis: for F being BinOp of D
for p being FinSequence of D st F . (e,d) = e holds
F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)
let F be BinOp of D; ::_thesis: for p being FinSequence of D st F . (e,d) = e holds
F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)
let p be FinSequence of D; ::_thesis: ( F . (e,d) = e implies F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e) )
assume A1: F . (e,d) = e ; ::_thesis: F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)
now__::_thesis:_for_i_being_Element_of_NAT_holds_(F_[:]_(([#]_(p,e)),d))_._i_=_([#]_((F_[:]_(p,d)),e))_._i
let i be Element of NAT ; ::_thesis: (F [:] (([#] (p,e)),d)) . i = ([#] ((F [:] (p,d)),e)) . i
A2: dom p = Seg (len p) by FINSEQ_1:def_3;
A3: ( len (F [:] (p,d)) = len p & dom (F [:] (p,d)) = Seg (len (F [:] (p,d))) ) by FINSEQ_1:def_3, FINSEQ_2:84;
now__::_thesis:_F_._((([#]_(p,e))_._i),d)_=_([#]_((F_[:]_(p,d)),e))_._i
percases ( i in dom p or not i in dom p ) ;
supposeA4: i in dom p ; ::_thesis: F . ((([#] (p,e)) . i),d) = ([#] ((F [:] (p,d)),e)) . i
hence F . ((([#] (p,e)) . i),d) = F . ((p . i),d) by Th20
.= (F [:] (p,d)) . i by A3, A2, A4, FUNCOP_1:27
.= ([#] ((F [:] (p,d)),e)) . i by A3, A2, A4, Th20 ;
::_thesis: verum
end;
supposeA5: not i in dom p ; ::_thesis: F . ((([#] (p,e)) . i),d) = ([#] ((F [:] (p,d)),e)) . i
hence F . ((([#] (p,e)) . i),d) = F . (e,d) by Th20
.= ([#] ((F [:] (p,d)),e)) . i by A1, A3, A2, A5, Th20 ;
::_thesis: verum
end;
end;
end;
hence  (F [:] (([#] (p,e)),d)) . i = ([#] ((F [:] (p,d)),e)) . i by FUNCOP_1:48; ::_thesis: verum
end;
hence  F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e) by FUNCT_2:63; ::_thesis: verum
end;

Lm6:  for D being non empty set
for d, e being Element of D
for F being BinOp of D
for p being FinSequence of D st F . (d,e) = e holds
F [;] (d,([#] (p,e))) = [#] ((F [;] (d,p)),e)
proof
let D be non empty set ; ::_thesis: for d, e being Element of D
for F being BinOp of D
for p being FinSequence of D st F . (d,e) = e holds
F [;] (d,([#] (p,e))) = [#] ((F [;] (d,p)),e)
let d, e be Element of D; ::_thesis: for F being BinOp of D
for p being FinSequence of D st F . (d,e) = e holds
F [;] (d,([#] (p,e))) = [#] ((F [;] (d,p)),e)
let F be BinOp of D; ::_thesis: for p being FinSequence of D st F . (d,e) = e holds
F [;] (d,([#] (p,e))) = [#] ((F [;] (d,p)),e)
let p be FinSequence of D; ::_thesis: ( F . (d,e) = e implies F [;] (d,([#] (p,e))) = [#] ((F [;] (d,p)),e) )
assume A1: F . (d,e) = e ; ::_thesis: F [;] (d,([#] (p,e))) = [#] ((F [;] (d,p)),e)
now__::_thesis:_for_i_being_Element_of_NAT_holds_(F_[;]_(d,([#]_(p,e))))_._i_=_([#]_((F_[;]_(d,p)),e))_._i
let i be Element of NAT ; ::_thesis: (F [;] (d,([#] (p,e)))) . i = ([#] ((F [;] (d,p)),e)) . i
A2: dom p = Seg (len p) by FINSEQ_1:def_3;
A3: ( len (F [;] (d,p)) = len p & dom (F [;] (d,p)) = Seg (len (F [;] (d,p))) ) by FINSEQ_1:def_3, FINSEQ_2:78;
now__::_thesis:_F_._(d,(([#]_(p,e))_._i))_=_([#]_((F_[;]_(d,p)),e))_._i
percases ( i in dom p or not i in dom p ) ;
supposeA4: i in dom p ; ::_thesis: F . (d,(([#] (p,e)) . i)) = ([#] ((F [;] (d,p)),e)) . i
hence F . (d,(([#] (p,e)) . i)) = F . (d,(p . i)) by Th20
.= (F [;] (d,p)) . i by A3, A2, A4, FUNCOP_1:32
.= ([#] ((F [;] (d,p)),e)) . i by A3, A2, A4, Th20 ;
::_thesis: verum
end;
supposeA5: not i in dom p ; ::_thesis: F . (d,(([#] (p,e)) . i)) = ([#] ((F [;] (d,p)),e)) . i
hence F . (d,(([#] (p,e)) . i)) = F . (d,e) by Th20
.= ([#] ((F [;] (d,p)),e)) . i by A1, A3, A2, A5, Th20 ;
::_thesis: verum
end;
end;
end;
hence  (F [;] (d,([#] (p,e)))) . i = ([#] ((F [;] (d,p)),e)) . i by FUNCOP_1:53; ::_thesis: verum
end;
hence  F [;] (d,([#] (p,e))) = [#] ((F [;] (d,p)),e) by FUNCT_2:63; ::_thesis: verum
end;

notation
let i be Nat;
synonym  finSeg i for  Seg i;
end;

definition
let i be Nat;
:: original: finSeg
redefine func finSeg i ->  Element of Fin NAT;
coherence
 finSeg i is Element of Fin NAT by Lm1;
end;

notation
let D be non empty set ;
let p be FinSequence of D;
let F be BinOp of D;
synonym F $$ p for F "**" p;
end;

definition
let D be non empty set ;
let p be FinSequence of D;
let F be BinOp of D;
assume A1: ( ( F is having_a_unity or len p >= 1 ) & F is associative & F is commutative ) ;
redefine func F "**" p equals :Def2: :: SETWOP_2:def 2
F $$ ((findom p),([#] (p,(the_unity_wrt F))));
compatibility
 for b1 being Element of D holds
( b1 = F $$ p iff b1 = F $$ ((findom p),([#] (p,(the_unity_wrt F)))) ) by A1, FINSOP_1:3;
end;

:: deftheorem Def2 defines $$ SETWOP_2:def_2_:_
 for D being non empty set
for p being FinSequence of D
for F being BinOp of D st ( F is having_a_unity or len p >= 1 ) & F is associative & F is commutative holds
F $$ p = F $$ ((findom p),([#] (p,(the_unity_wrt F))));

theorem Th25: :: SETWOP_2:25
for D being non empty set
for F being BinOp of D
for i being Nat st F is having_a_unity holds
F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F
proof
let D be non empty set ; ::_thesis: for F being BinOp of D
for i being Nat st F is having_a_unity holds
F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F
let F be BinOp of D; ::_thesis: for i being Nat st F is having_a_unity holds
F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F
let i be Nat; ::_thesis: ( F is having_a_unity implies F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F )
set e = the_unity_wrt F;
defpred S1[ Nat] means F "**" ($1 |-> (the_unity_wrt F)) = the_unity_wrt F;
assume A1: F is having_a_unity ; ::_thesis: F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F
A2: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A3: F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F ; ::_thesis: S1[i + 1]
thus F "**" ((i + 1) |-> (the_unity_wrt F)) = F "**" ((i |-> (the_unity_wrt F)) ^ <*(the_unity_wrt F)*>) by FINSEQ_2:60
.= F . ((F "**" (i |-> (the_unity_wrt F))),(the_unity_wrt F)) by A1, FINSOP_1:4
.= the_unity_wrt F by A1, A3, SETWISEO:15 ; ::_thesis: verum
end;
F "**" (0 |-> (the_unity_wrt F)) = F "**" (<*> D)
.= the_unity_wrt F by A1, FINSOP_1:10 ;
then A4: S1[ 0 ] ;
 for i being Nat holds S1[i] from NAT_1:sch_2(A4, A2);
hence  F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F ; ::_thesis: verum
end;

theorem Th26: :: SETWOP_2:26
for D being non empty set
for d being Element of D
for F being BinOp of D
for i, j being Nat st F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds
F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d)))
proof
let D be non empty set ; ::_thesis: for d being Element of D
for F being BinOp of D
for i, j being Nat st F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds
F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d)))
let d be Element of D; ::_thesis: for F being BinOp of D
for i, j being Nat st F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds
F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d)))
let F be BinOp of D; ::_thesis: for i, j being Nat st F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds
F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d)))
let i, j be Nat; ::_thesis: ( F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) implies F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d))) )
assume A1: F is associative ; ::_thesis: ( ( not ( i >= 1 & j >= 1 ) & not F is having_a_unity ) or F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d))) )
set p1 = i |-> d;
set p2 = j |-> d;
assume  ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) ; ::_thesis: F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d)))
then  ( ( len (i |-> d) >= 1 & len (j |-> d) >= 1 ) or F is having_a_unity ) by CARD_1:def_7;
then  F "**" ((i |-> d) ^ (j |-> d)) = F . ((F "**" (i |-> d)),(F "**" (j |-> d))) by A1, FINSOP_1:5;
hence  F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d))) by FINSEQ_2:123; ::_thesis: verum
end;

theorem :: SETWOP_2:27
for D being non empty set
for d being Element of D
for F being BinOp of D
for i, j being Nat st F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds
F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))
proof
let D be non empty set ; ::_thesis: for d being Element of D
for F being BinOp of D
for i, j being Nat st F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds
F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))
let d be Element of D; ::_thesis: for F being BinOp of D
for i, j being Nat st F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds
F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))
let F be BinOp of D; ::_thesis: for i, j being Nat st F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds
F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))
let i, j be Nat; ::_thesis: ( F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) implies F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) )
assume that
A1: ( F is commutative & F is associative ) and
A2: ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) ; ::_thesis: F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))
percases ( i = 0 or j = 0 or ( i > 0 & j > 0 ) ) by NAT_1:3;
supposeA3: ( i = 0 or j = 0 ) ; ::_thesis: F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))
set e = the_unity_wrt F;
A4: now__::_thesis:_F_"**"_(j_|->_(F_"**"_(i_|->_d)))_=_the_unity_wrt_F
percases ( i = 0 or j = 0 ) by A3;
suppose i = 0 ; ::_thesis: F "**" (j |-> (F "**" (i |-> d))) = the_unity_wrt F
then  i |-> d = <*> D ;
then  F "**" (i |-> d) = the_unity_wrt F by A2, A3, FINSOP_1:10;
hence  F "**" (j |-> (F "**" (i |-> d))) = the_unity_wrt F by A2, A3, Th25; ::_thesis: verum
end;
suppose j = 0 ; ::_thesis: F "**" (j |-> (F "**" (i |-> d))) = the_unity_wrt F
then  j |-> (F "**" (i |-> d)) = <*> D ;
hence  F "**" (j |-> (F "**" (i |-> d))) = the_unity_wrt F by A2, A3, FINSOP_1:10; ::_thesis: verum
end;
end;
end;
 (i * j) |-> d = <*> D by A3;
hence  F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) by A2, A3, A4, FINSOP_1:10; ::_thesis: verum
end;
supposeA5: ( i > 0 & j > 0 ) ; ::_thesis: F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))
defpred S1[ Nat] means ( $1 <> 0 implies F "**" ((i * $1) |-> d) = F "**" ($1 |-> (F "**" (i |-> d))) );
A6: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A7: ( j <> 0 implies F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) ) ; ::_thesis: S1[j + 1]
now__::_thesis:_S1[j_+_1]
percases ( j = 0 or j >= 1 + 0 ) by NAT_1:14;
supposeA8: j = 0 ; ::_thesis: S1[j + 1]
 1 |-> (F "**" (i |-> d)) = <*(F "**" (i |-> d))*> by FINSEQ_2:59;
hence  S1[j + 1] by A8, FINSOP_1:11; ::_thesis: verum
end;
supposeA9: j >= 1 + 0 ; ::_thesis: S1[j + 1]
then  j > 0 by NAT_1:13;
then  i * j > i * 0 by A5, XREAL_1:68;
then A10: i * j >= 1 + 0 by NAT_1:13;
F "**" ((i * (j + 1)) |-> d) = F "**" (((i * j) + (i * 1)) |-> d)
.= F . ((F "**" ((i * j) |-> d)),(F "**" (i |-> d))) by A1, A2, A10, Th26
.= F . ((F "**" ((i * j) |-> d)),(F "**" (1 |-> (F "**" (i |-> d))))) by FINSOP_1:16
.= F "**" ((j + 1) |-> (F "**" (i |-> d))) by A1, A7, A9, Th26 ;
hence  S1[j + 1] ; ::_thesis: verum
end;
end;
end;
hence  S1[j + 1] ; ::_thesis: verum
end;
A11: S1[ 0 ] ;
 for j being Nat holds S1[j] from NAT_1:sch_2(A11, A6);
hence  F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) by A5; ::_thesis: verum
end;
end;
end;

theorem Th28: :: SETWOP_2:28
for E, D being non empty set
for F being BinOp of D
for H being BinOp of E
for h being Function of D,E
for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h . (F "**" p) = H "**" (h * p)
proof
let E, D be non empty set ; ::_thesis: for F being BinOp of D
for H being BinOp of E
for h being Function of D,E
for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h . (F "**" p) = H "**" (h * p)
let F be BinOp of D; ::_thesis: for H being BinOp of E
for h being Function of D,E
for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h . (F "**" p) = H "**" (h * p)
let H be BinOp of E; ::_thesis: for h being Function of D,E
for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h . (F "**" p) = H "**" (h * p)
let h be Function of D,E; ::_thesis: for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h . (F "**" p) = H "**" (h * p)
let p be FinSequence of D; ::_thesis: ( F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h . (F "**" p) = H "**" (h * p) )
assume that
A1: F is having_a_unity and
A2: H is having_a_unity and
A3: h . (the_unity_wrt F) = the_unity_wrt H and
A4: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; ::_thesis: h . (F "**" p) = H "**" (h * p)
defpred S1[ FinSequence of D] means h . (F "**" $1) = H "**" (h * $1);
A5: 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 A6: h . (F "**" q) = H "**" (h * q) ; ::_thesis: S1[q ^ <*d*>]
thus h . (F "**" (q ^ <*d*>)) = h . (F . ((F "**" q),d)) by A1, FINSOP_1:4
.= H . ((H "**" (h * q)),(h . d)) by A4, A6
.= H "**" ((h * q) ^ <*(h . d)*>) by A2, FINSOP_1:4
.= H "**" (h * (q ^ <*d*>)) by FINSEQOP:8 ; ::_thesis: verum
end;
h . (F "**" (<*> D)) = h . (the_unity_wrt F) by A1, FINSOP_1:10
.= H "**" (<*> E) by A2, A3, FINSOP_1:10
.= H "**" (h * (<*> D)) ;
then A7: S1[ <*> D] ;
 for q being FinSequence of D holds S1[q] from FINSEQ_2:sch_2(A7, A5);
hence  h . (F "**" p) = H "**" (h * p) ; ::_thesis: verum
end;

theorem :: SETWOP_2:29
for D being non empty set
for F being BinOp of D
for u being UnOp of D
for p being FinSequence of D st F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F holds
u . (F "**" p) = F "**" (u * p)
proof
let D be non empty set ; ::_thesis: for F being BinOp of D
for u being UnOp of D
for p being FinSequence of D st F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F holds
u . (F "**" p) = F "**" (u * p)
let F be BinOp of D; ::_thesis: for u being UnOp of D
for p being FinSequence of D st F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F holds
u . (F "**" p) = F "**" (u * p)
let u be UnOp of D; ::_thesis: for p being FinSequence of D st F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F holds
u . (F "**" p) = F "**" (u * p)
let p be FinSequence of D; ::_thesis: ( F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F implies u . (F "**" p) = F "**" (u * p) )
assume A1: ( F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F ) ; ::_thesis: ( not u is_distributive_wrt F or u . (F "**" p) = F "**" (u * p) )
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 "**" p) = F "**" (u * p)
hence  u . (F "**" p) = F "**" (u * p) by A1, Th28; ::_thesis: verum
end;

theorem :: SETWOP_2:30
for D being non empty set
for d being Element of D
for F, G being BinOp of D
for p being FinSequence 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))) . (F "**" p) = F "**" ((G [;] (d,(id D))) * p)
proof
let D be non empty set ; ::_thesis: for d being Element of D
for F, G being BinOp of D
for p being FinSequence 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))) . (F "**" p) = F "**" ((G [;] (d,(id D))) * p)
let d be Element of D; ::_thesis: for F, G being BinOp of D
for p being FinSequence 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))) . (F "**" p) = F "**" ((G [;] (d,(id D))) * p)
let F, G be BinOp of D; ::_thesis: for p being FinSequence 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))) . (F "**" p) = F "**" ((G [;] (d,(id D))) * p)
let p be FinSequence 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))) . (F "**" p) = F "**" ((G [;] (d,(id D))) * p) )
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))) . (F "**" p) = F "**" ((G [;] (d,(id D))) * p)
set e = the_unity_wrt F;
set u = G [;] (d,(id D));
 G [;] (d,(id D)) is_distributive_wrt F by A4, FINSEQOP:54;
then A5: for d1, d2 being Element of D holds (G [;] (d,(id D))) . (F . (d1,d2)) = F . (((G [;] (d,(id D))) . d1),((G [;] (d,(id D))) . d2)) by BINOP_1:def_12;
 (G [;] (d,(id D))) . (the_unity_wrt F) = the_unity_wrt F by A1, A2, A3, A4, FINSEQOP:69;
hence  (G [;] (d,(id D))) . (F "**" p) = F "**" ((G [;] (d,(id D))) * p) by A2, A5, Th28; ::_thesis: verum
end;

theorem :: SETWOP_2:31
for D being non empty set
for F being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp holds
(the_inverseOp_wrt F) . (F "**" p) = F "**" ((the_inverseOp_wrt F) * p)
proof
let D be non empty set ; ::_thesis: for F being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp holds
(the_inverseOp_wrt F) . (F "**" p) = F "**" ((the_inverseOp_wrt F) * p)
let F be BinOp of D; ::_thesis: for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp holds
(the_inverseOp_wrt F) . (F "**" p) = F "**" ((the_inverseOp_wrt F) * p)
let p be FinSequence of D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp implies (the_inverseOp_wrt F) . (F "**" p) = F "**" ((the_inverseOp_wrt F) * p) )
assume that
A1: ( F is commutative & F is associative ) and
A2: F is having_a_unity and
A3: F is having_an_inverseOp ; ::_thesis: (the_inverseOp_wrt F) . (F "**" p) = F "**" ((the_inverseOp_wrt F) * p)
set e = the_unity_wrt F;
set u = the_inverseOp_wrt F;
 the_inverseOp_wrt F is_distributive_wrt F by A1, A2, A3, FINSEQOP:63;
then A4: for d1, d2 being Element of D holds (the_inverseOp_wrt F) . (F . (d1,d2)) = F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . d2)) by BINOP_1:def_12;
 (the_inverseOp_wrt F) . (the_unity_wrt F) = the_unity_wrt F by A1, A2, A3, FINSEQOP:61;
hence  (the_inverseOp_wrt F) . (F "**" p) = F "**" ((the_inverseOp_wrt F) * p) by A2, A4, Th28; ::_thesis: verum
end;

theorem Th32: :: SETWOP_2:32
for D being non empty set
for e being Element of D
for F, G being BinOp of D
for p, q being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) & len p = len q holds
G . ((F "**" p),(F "**" q)) = F "**" (G .: (p,q))
proof
let D be non empty set ; ::_thesis: for e being Element of D
for F, G being BinOp of D
for p, q being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) & len p = len q holds
G . ((F "**" p),(F "**" q)) = F "**" (G .: (p,q))
let e be Element of D; ::_thesis: for F, G being BinOp of D
for p, q being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) & len p = len q holds
G . ((F "**" p),(F "**" q)) = F "**" (G .: (p,q))
let F, G be BinOp of D; ::_thesis: for p, q being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) & len p = len q holds
G . ((F "**" p),(F "**" q)) = F "**" (G .: (p,q))
let p, q be FinSequence of D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) & len p = len q implies G . ((F "**" p),(F "**" q)) = F "**" (G .: (p,q)) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F ) and
A2: G . (e,e) = e and
A3: for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) and
A4: len p = len q ; ::_thesis: G . ((F "**" p),(F "**" q)) = F "**" (G .: (p,q))
A5: len p = len (G .: (p,q)) by A4, FINSEQ_2:72;
A6: dom (G .: (p,q)) = Seg (len (G .: (p,q))) by FINSEQ_1:def_3;
A7: dom q = Seg (len q) by FINSEQ_1:def_3;
A8: dom p = Seg (len p) by FINSEQ_1:def_3;
thus G . ((F "**" p),(F "**" q)) = G . ((F $$ ((findom p),([#] (p,e)))),(F "**" q)) by A1, Def2
.= G . ((F $$ ((findom p),([#] (p,e)))),(F $$ ((findom q),([#] (q,e))))) by A1, Def2
.= F $$ ((findom p),(G .: (([#] (p,e)),([#] (q,e))))) by A1, A2, A3, A4, A8, A7, Th9
.= F $$ ((findom (G .: (p,q))),([#] ((G .: (p,q)),e))) by A2, A4, A5, A8, A6, Lm4
.= F "**" (G .: (p,q)) by A1, Def2 ; ::_thesis: verum
end;

theorem Th33: :: SETWOP_2:33
for D being non empty set
for e being Element of D
for F, G being BinOp of D
for i being Nat
for T1, T2 being Element of i -tuples_on D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds
G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2))
proof
let D be non empty set ; ::_thesis: for e being Element of D
for F, G being BinOp of D
for i being Nat
for T1, T2 being Element of i -tuples_on D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds
G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2))
let e be Element of D; ::_thesis: for F, G being BinOp of D
for i being Nat
for T1, T2 being Element of i -tuples_on D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds
G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2))
let F, G be BinOp of D; ::_thesis: for i being Nat
for T1, T2 being Element of i -tuples_on D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds
G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2))
let i be Nat; ::_thesis: for T1, T2 being Element of i -tuples_on D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds
G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2))
let T1, T2 be Element of i -tuples_on D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) implies G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2)) )
 ( len T1 = i & len T2 = i ) by CARD_1:def_7;
hence  ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) implies G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2)) ) by Th32; ::_thesis: verum
end;

theorem Th34: :: SETWOP_2:34
for D being non empty set
for F being BinOp of D
for p, q being FinSequence of D st F is commutative & F is associative & F is having_a_unity & len p = len q holds
F . ((F "**" p),(F "**" q)) = F "**" (F .: (p,q))
proof
let D be non empty set ; ::_thesis: for F being BinOp of D
for p, q being FinSequence of D st F is commutative & F is associative & F is having_a_unity & len p = len q holds
F . ((F "**" p),(F "**" q)) = F "**" (F .: (p,q))
let F be BinOp of D; ::_thesis: for p, q being FinSequence of D st F is commutative & F is associative & F is having_a_unity & len p = len q holds
F . ((F "**" p),(F "**" q)) = F "**" (F .: (p,q))
let p, q be FinSequence of D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & len p = len q implies F . ((F "**" p),(F "**" q)) = F "**" (F .: (p,q)) )
set e = the_unity_wrt F;
assume A1: ( F is commutative & F is associative & F is having_a_unity ) ; ::_thesis: ( not len p = len q or F . ((F "**" p),(F "**" q)) = F "**" (F .: (p,q)) )
then  ( F . ((the_unity_wrt F),(the_unity_wrt F)) = the_unity_wrt F & ( for d1, d2, d3, d4 being Element of D holds F . ((F . (d1,d2)),(F . (d3,d4))) = F . ((F . (d1,d3)),(F . (d2,d4))) ) ) by Lm3, SETWISEO:15;
hence  ( not len p = len q or F . ((F "**" p),(F "**" q)) = F "**" (F .: (p,q)) ) by A1, Th32; ::_thesis: verum
end;

theorem Th35: :: SETWOP_2:35
for D being non empty set
for F being BinOp of D
for i being Nat
for T1, T2 being Element of i -tuples_on D st F is commutative & F is associative & F is having_a_unity holds
F . ((F "**" T1),(F "**" T2)) = F "**" (F .: (T1,T2))
proof
let D be non empty set ; ::_thesis: for F being BinOp of D
for i being Nat
for T1, T2 being Element of i -tuples_on D st F is commutative & F is associative & F is having_a_unity holds
F . ((F "**" T1),(F "**" T2)) = F "**" (F .: (T1,T2))
let F be BinOp of D; ::_thesis: for i being Nat
for T1, T2 being Element of i -tuples_on D st F is commutative & F is associative & F is having_a_unity holds
F . ((F "**" T1),(F "**" T2)) = F "**" (F .: (T1,T2))
let i be Nat; ::_thesis: for T1, T2 being Element of i -tuples_on D st F is commutative & F is associative & F is having_a_unity holds
F . ((F "**" T1),(F "**" T2)) = F "**" (F .: (T1,T2))
let T1, T2 be Element of i -tuples_on D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity implies F . ((F "**" T1),(F "**" T2)) = F "**" (F .: (T1,T2)) )
 ( len T1 = i & len T2 = i ) by CARD_1:def_7;
hence  ( F is commutative & F is associative & F is having_a_unity implies F . ((F "**" T1),(F "**" T2)) = F "**" (F .: (T1,T2)) ) by Th34; ::_thesis: verum
end;

theorem :: SETWOP_2:36
for D being non empty set
for d1, d2 being Element of D
for F being BinOp of D
for i being Nat st F is commutative & F is associative & F is having_a_unity holds
F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2)))
proof
let D be non empty set ; ::_thesis: for d1, d2 being Element of D
for F being BinOp of D
for i being Nat st F is commutative & F is associative & F is having_a_unity holds
F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2)))
let d1, d2 be Element of D; ::_thesis: for F being BinOp of D
for i being Nat st F is commutative & F is associative & F is having_a_unity holds
F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2)))
let F be BinOp of D; ::_thesis: for i being Nat st F is commutative & F is associative & F is having_a_unity holds
F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2)))
let i be Nat; ::_thesis: ( F is commutative & F is associative & F is having_a_unity implies F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2))) )
reconsider T1 = i |-> d1, T2 = i |-> d2 as Element of i -tuples_on D ;
 i |-> (F . (d1,d2)) = F .: (T1,T2) by FINSEQOP:17;
hence  ( F is commutative & F is associative & F is having_a_unity implies F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2))) ) by Th35; ::_thesis: verum
end;

theorem :: SETWOP_2:37
for D being non empty set
for F, G being BinOp of D
for i being Nat
for T1, T2 being Element of i -tuples_on 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
G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2))
proof
let D be non empty set ; ::_thesis: for F, G being BinOp of D
for i being Nat
for T1, T2 being Element of i -tuples_on 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
G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2))
let F, G be BinOp of D; ::_thesis: for i being Nat
for T1, T2 being Element of i -tuples_on 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
G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2))
let i be Nat; ::_thesis: for T1, T2 being Element of i -tuples_on 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
G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2))
let T1, T2 be Element of i -tuples_on 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 G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2)) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: ( F is having_an_inverseOp & G = F * ((id D),(the_inverseOp_wrt F)) ) ; ::_thesis: G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2))
set e = the_unity_wrt F;
 ( G . ((the_unity_wrt F),(the_unity_wrt F)) = the_unity_wrt F & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) ) by A1, A2, FINSEQOP:86, FINSEQOP:89;
hence  G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2)) by A1, Th33; ::_thesis: verum
end;

theorem Th38: :: SETWOP_2:38
for D being non empty set
for e, d being Element of D
for F, G being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (d,e) = e holds
G . (d,(F "**" p)) = F "**" (G [;] (d,p))
proof
let D be non empty set ; ::_thesis: for e, d being Element of D
for F, G being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (d,e) = e holds
G . (d,(F "**" p)) = F "**" (G [;] (d,p))
let e, d be Element of D; ::_thesis: for F, G being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (d,e) = e holds
G . (d,(F "**" p)) = F "**" (G [;] (d,p))
let F, G be BinOp of D; ::_thesis: for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (d,e) = e holds
G . (d,(F "**" p)) = F "**" (G [;] (d,p))
let p be FinSequence of D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (d,e) = e implies G . (d,(F "**" p)) = F "**" (G [;] (d,p)) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F ) and
A2: G is_distributive_wrt F and
A3: G . (d,e) = e ; ::_thesis: G . (d,(F "**" p)) = F "**" (G [;] (d,p))
A4: ( len p = len (G [;] (d,p)) & Seg (len p) = dom p ) by FINSEQ_1:def_3, FINSEQ_2:78;
A5: Seg (len (G [;] (d,p))) = dom (G [;] (d,p)) by FINSEQ_1:def_3;
thus G . (d,(F "**" p)) = G . (d,(F $$ ((findom p),([#] (p,e))))) by A1, Def2
.= F $$ ((findom p),(G [;] (d,([#] (p,e))))) by A1, A2, A3, Th12
.= F $$ ((findom p),([#] ((G [;] (d,p)),e))) by A3, Lm6
.= F "**" (G [;] (d,p)) by A1, A4, A5, Def2 ; ::_thesis: verum
end;

theorem Th39: :: SETWOP_2:39
for D being non empty set
for e, d being Element of D
for F, G being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F "**" p),d) = F "**" (G [:] (p,d))
proof
let D be non empty set ; ::_thesis: for e, d being Element of D
for F, G being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F "**" p),d) = F "**" (G [:] (p,d))
let e, d be Element of D; ::_thesis: for F, G being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F "**" p),d) = F "**" (G [:] (p,d))
let F, G be BinOp of D; ::_thesis: for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F "**" p),d) = F "**" (G [:] (p,d))
let p be FinSequence of D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e implies G . ((F "**" p),d) = F "**" (G [:] (p,d)) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F ) and
A2: G is_distributive_wrt F and
A3: G . (e,d) = e ; ::_thesis: G . ((F "**" p),d) = F "**" (G [:] (p,d))
A4: ( len p = len (G [:] (p,d)) & Seg (len p) = dom p ) by FINSEQ_1:def_3, FINSEQ_2:84;
A5: Seg (len (G [:] (p,d))) = dom (G [:] (p,d)) by FINSEQ_1:def_3;
thus G . ((F "**" p),d) = G . ((F $$ ((findom p),([#] (p,e)))),d) by A1, Def2
.= F $$ ((findom p),(G [:] (([#] (p,e)),d))) by A1, A2, A3, Th13
.= F $$ ((findom p),([#] ((G [:] (p,d)),e))) by A3, Lm5
.= F "**" (G [:] (p,d)) by A1, A4, A5, Def2 ; ::_thesis: verum
end;

theorem :: SETWOP_2:40
for D being non empty set
for d being Element of D
for F, G being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . (d,(F "**" p)) = F "**" (G [;] (d,p))
proof
let D be non empty set ; ::_thesis: for d being Element of D
for F, G being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . (d,(F "**" p)) = F "**" (G [;] (d,p))
let d be Element of D; ::_thesis: for F, G being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . (d,(F "**" p)) = F "**" (G [;] (d,p))
let F, G be BinOp of D; ::_thesis: for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . (d,(F "**" p)) = F "**" (G [;] (d,p))
let p be FinSequence of D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies G . (d,(F "**" p)) = F "**" (G [;] (d,p)) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: F is having_an_inverseOp and
A3: G is_distributive_wrt F ; ::_thesis: G . (d,(F "**" p)) = F "**" (G [;] (d,p))
set e = the_unity_wrt F;
 G . (d,(the_unity_wrt F)) = the_unity_wrt F by A1, A2, A3, FINSEQOP:66;
hence  G . (d,(F "**" p)) = F "**" (G [;] (d,p)) by A1, A3, Th38; ::_thesis: verum
end;

theorem :: SETWOP_2:41
for D being non empty set
for d being Element of D
for F, G being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F "**" p),d) = F "**" (G [:] (p,d))
proof
let D be non empty set ; ::_thesis: for d being Element of D
for F, G being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F "**" p),d) = F "**" (G [:] (p,d))
let d be Element of D; ::_thesis: for F, G being BinOp of D
for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F "**" p),d) = F "**" (G [:] (p,d))
let F, G be BinOp of D; ::_thesis: for p being FinSequence of D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F "**" p),d) = F "**" (G [:] (p,d))
let p be FinSequence of D; ::_thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies G . ((F "**" p),d) = F "**" (G [:] (p,d)) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: F is having_an_inverseOp and
A3: G is_distributive_wrt F ; ::_thesis: G . ((F "**" p),d) = F "**" (G [:] (p,d))
set e = the_unity_wrt F;
 G . ((the_unity_wrt F),d) = the_unity_wrt F by A1, A2, A3, FINSEQOP:66;
hence  G . ((F "**" p),d) = F "**" (G [:] (p,d)) by A1, A3, Th39; ::_thesis: verum
end;