let C, D be 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))
let c be 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 B be 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 F be 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 Function of C,D; ( 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
; F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))
per cases
( B = {} or B <> {} )
;
suppose A4:
B = {}
;
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
;
verum end; suppose A5:
B <> {}
;
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;
for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]let c9 be
Element of
C;
( 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
;
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;
per cases
( B9 = {} or B9 <> {} )
;
suppose A22:
B9 <> {}
;
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
;
verum 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
;
verum end;