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