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 & F is having_a_unity ) and
A2: 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 );
A3: S₁[ {}. C] by RELAT_1:149;
A4: for B' being Element of Fin C
for b being Element of C st S₁[B'] & not b in B' holds
S₁[B' \/ {.b.}]

proof

let B' be Element of Fin C; :: thesis: for b being Element of C st S₁[B'] & not b in B' holds
S₁[B' \/ {.b.}]
let c be Element of C; :: thesis: ( S₁[B'] & not c in B' implies S₁[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} ; :: thesis: F $$ (B' \/ {.c.}),f = e
{.c.} c= C by FINSUB_1:def 5;
then ( {c} c= B' \/ {c} & {c} c= dom f & {c} <> {} ) by FUNCT_2:def 1, XBOOLE_1:7;
then ( Im f,c c= {e} & Im f,c <> {} & c in dom f ) by A7, RELAT_1:156, ZFMISC_1:37;
then ( Im f,c = {e} & c in dom f ) by ZFMISC_1:39;
then {e} = {(f . c)} by FUNCT_1:117;
then A8: f . c = e by ZFMISC_1:6;

now

per cases ( B' = {} or B' <> {} ) ;

suppose B' = {} ; :: thesis: 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, A6, Th4
.= F . e,(f . c) by A1, A2, A9, SETWISEO:40 ; :: thesis: verum

end;

suppose A10: B' <> {} ; :: thesis: F $$ (B' \/ {.c.}),f = F . e,(f . c)

B' c= C by FINSUB_1:def 5;
then ( B' c= B' \/ {c} & B' c= dom f ) by FUNCT_2:def 1, XBOOLE_1:7;
then ( f .: B' c= {e} & f .: B' <> {} ) by A7, A10, RELAT_1:156;
hence F $$ (B' \/ {.c.}),f = F . e,(f . c) by A1, A5, A6, Th4, ZFMISC_1:39; :: thesis: verum

end;

end;

end;

hence F $$ (B' \/ {.c.}),f = e by A1, A2, A8, SETWISEO:23; :: thesis: verum

end;

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