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 B' being Element of Fin C
for b being Element of C st S1[B'] & not b in B' holds
S1[B' \/ {.b.}]
proof
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 A5:
(
f .: B' = {e} implies
F $$ B',
f = e )
and A6:
not
c in B'
and A7:
f .: (B' \/ {c}) = {e}
;
F $$ (B' \/ {.c.}),f = e
A8:
now per cases
( B' = {} or B' <> {} )
;
suppose
B' = {}
;
F $$ (B' \/ {.c.}),f = F . e,(f . c)then A9:
B' = {}. C
;
thus F $$ (B' \/ {.c.}),
f =
F . (F $$ B',f),
(f . c)
by A1, A2, A6, Th4
.=
F . e,
(f . c)
by A1, A2, A3, A9, SETWISEO:40
;
verum end; suppose A10:
B' <> {}
;
F $$ (B' \/ {.c.}),f = F . e,(f . c)
B' c= C
by FINSUB_1:def 5;
then A11:
B' c= dom f
by FUNCT_2:def 1;
f .: B' c= {e}
by A7, RELAT_1:156, XBOOLE_1:7;
hence
F $$ (B' \/ {.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 $$ (B' \/ {.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