let C, D be 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
let B be 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 e be 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 F be 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 Function of C,D; ( 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
; ( 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;
for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]let c be
Element of
C;
( 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}
;
F $$ (B9 \/ {.c.}),f = e
A8:
now per cases
( B9 = {} or B9 <> {} )
;
suppose
B9 = {}
;
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, Th4
.=
F . e,
(f . c)
by A1, A2, A3, A9, SETWISEO:40
;
verum end; suppose A10:
B9 <> {}
;
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:156, XBOOLE_1:7;
hence
F $$ (B9 \/ {.c.}),
f = F . e,
(f . c)
by A1, A5, A6, A10, A11, Th4, ZFMISC_1:39;
verum 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:37;
Im f,
c c= {e}
by A7, RELAT_1:156, XBOOLE_1:7;
then
Im f,
c = {e}
by A12, ZFMISC_1:39;
then
{e} = {(f . c)}
by A13, FUNCT_1:117;
then
f . c = e
by ZFMISC_1:6;
hence
F $$ (B9 \/ {.c.}),
f = e
by A2, A3, A8, SETWISEO:23;
verum
end;
A14:
S1[ {}. C]
by RELAT_1:149;
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 )
; verum