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 S_{1}[ 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 S_{1}[B9] & not b in B9 holds

S_{1}[B9 \/ {.b.}]
_{1}[ {}. C]
;

for B being Element of Fin C holds S_{1}[B]
from SETWISEO:sch 2(A14, A4);

hence ( not f .: B = {e} or F $$ (B,f) = e ) ; :: thesis: verum

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 S

A4: for B9 being Element of Fin C

for b being Element of C st S

S

proof

A14:
S
let B9 be Element of Fin C; :: thesis: for b being Element of C st S_{1}[B9] & not b in B9 holds

S_{1}[B9 \/ {.b.}]

let c be Element of C; :: thesis: ( S_{1}[B9] & not c in B9 implies S_{1}[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

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

let c be Element of C; :: thesis: ( S

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))

{.c.} c= C
by FINSUB_1:def 5;end;

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

for B being Element of Fin C holds S

hence ( not f .: B = {e} or F $$ (B,f) = e ) ; :: thesis: verum