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:40;
hence F . (F $$ B,f),
(f . c) =
f . c
by A2, A4, SETWISEO:23
.=
F $$ (B \/ {.c.}),
f
by A1, A4, SETWISEO:26
;
verum end; suppose A5:
B <> {}
;
F $$ (B \/ {.c.}),f = F . (F $$ B,f),(f . c)consider g' being
Function of
Fin C,
D such that A6:
F $$ B,
f = g' . B
and
for
e being
Element of
D st
e is_a_unity_wrt F holds
g' . {} = e
and A7:
for
c' being
Element of
C holds
g' . {c'} = f . c'
and A8:
for
B' being
Element of
Fin C st
B' c= B &
B' <> {} holds
for
c' being
Element of
C st
c' in B \ B' holds
g' . (B' \/ {c'}) = F . (g' . B'),
(f . c')
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
c' being
Element of
C holds
g . {c'} = f . c'
and A11:
for
B' being
Element of
Fin C st
B' c= B \/ {c} &
B' <> {} holds
for
c' being
Element of
C st
c' in (B \/ {c}) \ B' holds
g . (B' \/ {c'}) = F . (g . B'),
(f . c')
by A1, SETWISEO:def 3;
defpred S1[
set ]
means ( $1
<> {} & $1
c= B implies
g . $1
= g' . $1 );
A12:
for
B' being
Element of
Fin C for
b being
Element of
C st
S1[
B'] & not
b in B' holds
S1[
B' \/ {b}]
proof
A13:
B c= B \/ {c}
by XBOOLE_1:7;
let B' be
Element of
Fin C;
for b being Element of C st S1[B'] & not b in B' holds
S1[B' \/ {b}]let c' be
Element of
C;
( S1[B'] & not c' in B' implies S1[B' \/ {c'}] )
assume that A14:
(
B' <> {} &
B' c= B implies
g . B' = g' . B' )
and A15:
not
c' in B'
and
B' \/ {c'} <> {}
and A16:
B' \/ {c'} c= B
;
g . (B' \/ {c'}) = g' . (B' \/ {c'})
A17:
c' in B
by A16, SETWISEO:8;
then A18:
c' in B \ B'
by A15, XBOOLE_0:def 5;
c' in B \/ {c}
by A17, XBOOLE_0:def 3;
then A19:
c' in (B \/ {c}) \ B'
by A15, XBOOLE_0:def 5;
B' c= B
by A16, XBOOLE_1:11;
then A20:
B' c= B \/ {c}
by A13, XBOOLE_1:1;
per cases
( B' = {} or B' <> {} )
;
suppose A22:
B' <> {}
;
g . (B' \/ {c'}) = g' . (B' \/ {c'})hence g . (B' \/ {c'}) =
F . (g' . B'),
(f . c')
by A11, A14, A16, A20, A19, XBOOLE_1:11
.=
g' . (B' \/ {c'})
by A8, A16, A18, A22, XBOOLE_1:11
;
verum end;
end; A23:
S1[
{}. C]
;
A24:
for
B' being
Element of
Fin C holds
S1[
B']
from SETWISEO:sch 2(A23, A12);
c in B \/ {c}
by SETWISEO:6;
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;