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₁[ 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₁[B9] & not b in B9 holds
S₁[B9 \/ {.b.}]

proof

let B9 be Element of Fin C; :: thesis: for b being Element of C st S₁[B9] & not b in B9 holds
S₁[B9 \/ {.b.}]
let c be Element of C; :: thesis: ( S₁[B9] & not c in B9 implies S₁[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

A8: now :: thesis: F $$ ((B9 \/ {.c.}),f) = F . (e,(f . c))

per cases ( B9 = {} or B9 <> {} ) ;

suppose B9 = {} ; :: thesis: 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, Th2
.= F . (e,(f . c)) by A1, A2, A3, A9, SETWISEO:31 ; :: thesis: verum

end;

suppose A10: B9 <> {} ; :: thesis: 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:123, XBOOLE_1:7;
hence F $$ ((B9 \/ {.c.}),f) = F . (e,(f . c)) by A1, A5, A6, A10, A11, Th2, ZFMISC_1:33; :: thesis: verum

end;

end;

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

A14: S₁[ {}. C] ;
for B being Element of Fin C holds S₁[B] from SETWISEO:sch 2(A14, A4);
hence ( not f .: B = {e} or F $$ (B,f) = e ) ; :: thesis: verum