let C, D be non empty set ; :: thesis: for c being Element of C

for B being Element of Fin C

for F being BinOp of D

for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds

F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))

let c be Element of C; :: thesis: for B being Element of Fin C

for F being BinOp of D

for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds

F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))

let B be Element of Fin C; :: thesis: for F being BinOp of D

for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds

F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))

let F be BinOp of D; :: thesis: for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds

F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))

let f be Function of C,D; :: thesis: ( F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B implies F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c)) )

assume that

A1: ( F is commutative & F is associative ) and

A2: ( B <> {} or F is having_a_unity ) and

A3: not c in B ; :: thesis: F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))

for B being Element of Fin C

for F being BinOp of D

for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds

F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))

let c be Element of C; :: thesis: for B being Element of Fin C

for F being BinOp of D

for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds

F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))

let B be Element of Fin C; :: thesis: for F being BinOp of D

for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds

F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))

let F be BinOp of D; :: thesis: for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds

F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))

let f be Function of C,D; :: thesis: ( F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B implies F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c)) )

assume that

A1: ( F is commutative & F is associative ) and

A2: ( B <> {} or F is having_a_unity ) and

A3: not c in B ; :: thesis: F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))

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

end;

suppose A4:
B = {}
; :: thesis: F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))

then
B = {}. C
;

then F $$ (B,f) = the_unity_wrt F by A1, A2, SETWISEO:31;

hence F . ((F $$ (B,f)),(f . c)) = f . c by A2, A4, SETWISEO:15

.= F $$ ((B \/ {.c.}),f) by A1, A4, SETWISEO:17 ;

:: thesis: verum

end;then F $$ (B,f) = the_unity_wrt F by A1, A2, SETWISEO:31;

hence F . ((F $$ (B,f)),(f . c)) = f . c by A2, A4, SETWISEO:15

.= F $$ ((B \/ {.c.}),f) by A1, A4, SETWISEO:17 ;

:: thesis: verum

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

consider g9 being Function of (Fin C),D such that

A6: F $$ (B,f) = g9 . B and

for e being Element of D st e is_a_unity_wrt F holds

g9 . {} = e and

A7: for c9 being Element of C holds g9 . {c9} = f . c9 and

A8: for B9 being Element of Fin C st B9 c= B & B9 <> {} holds

for c9 being Element of C st c9 in B \ B9 holds

g9 . (B9 \/ {c9}) = F . ((g9 . B9),(f . c9)) by A1, A2, SETWISEO:def 3;

consider g being Function of (Fin C),D such that

A9: F $$ ((B \/ {.c.}),f) = g . (B \/ {c}) and

for e being Element of D st e is_a_unity_wrt F holds

g . {} = e and

A10: for c9 being Element of C holds g . {c9} = f . c9 and

A11: for B9 being Element of Fin C st B9 c= B \/ {c} & B9 <> {} holds

for c9 being Element of C st c9 in (B \/ {c}) \ B9 holds

g . (B9 \/ {c9}) = F . ((g . B9),(f . c9)) by A1, SETWISEO:def 3;

defpred S_{1}[ set ] means ( $1 <> {} & $1 c= B implies g . $1 = g9 . $1 );

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

A24: for B9 being Element of Fin C holds S_{1}[B9]
from SETWISEO:sch 2(A23, A12);

c in B \/ {c} by ZFMISC_1:136;

then c in (B \/ {c}) \ B by A3, XBOOLE_0:def 5;

hence F $$ ((B \/ {.c.}),f) = F . ((g . B),(f . c)) by A5, A9, A11, XBOOLE_1:7

.= F . ((F $$ (B,f)),(f . c)) by A5, A6, A24 ;

:: thesis: verum

end;A6: F $$ (B,f) = g9 . B and

for e being Element of D st e is_a_unity_wrt F holds

g9 . {} = e and

A7: for c9 being Element of C holds g9 . {c9} = f . c9 and

A8: for B9 being Element of Fin C st B9 c= B & B9 <> {} holds

for c9 being Element of C st c9 in B \ B9 holds

g9 . (B9 \/ {c9}) = F . ((g9 . B9),(f . c9)) by A1, A2, SETWISEO:def 3;

consider g being Function of (Fin C),D such that

A9: F $$ ((B \/ {.c.}),f) = g . (B \/ {c}) and

for e being Element of D st e is_a_unity_wrt F holds

g . {} = e and

A10: for c9 being Element of C holds g . {c9} = f . c9 and

A11: for B9 being Element of Fin C st B9 c= B \/ {c} & B9 <> {} holds

for c9 being Element of C st c9 in (B \/ {c}) \ B9 holds

g . (B9 \/ {c9}) = F . ((g . B9),(f . c9)) by A1, SETWISEO:def 3;

defpred S

A12: for B9 being Element of Fin C

for b being Element of C st S

S

proof

A23:
S
A13:
B c= B \/ {c}
by XBOOLE_1:7;

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

assume that

A14: ( B9 <> {} & B9 c= B implies g . B9 = g9 . B9 ) and

A15: not c9 in B9 and

B9 \/ {c9} <> {} and

A16: B9 \/ {c9} c= B ; :: thesis: g . (B9 \/ {c9}) = g9 . (B9 \/ {c9})

A17: c9 in B by A16, ZFMISC_1:137;

then A18: c9 in B \ B9 by A15, XBOOLE_0:def 5;

c9 in B \/ {c} by A17, XBOOLE_0:def 3;

then A19: c9 in (B \/ {c}) \ B9 by A15, XBOOLE_0:def 5;

B9 c= B by A16, XBOOLE_1:11;

then A20: B9 c= B \/ {c} by A13, XBOOLE_1:1;

end;let B9 be Element of Fin C; :: thesis: for b being Element of C st S

S

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

assume that

A14: ( B9 <> {} & B9 c= B implies g . B9 = g9 . B9 ) and

A15: not c9 in B9 and

B9 \/ {c9} <> {} and

A16: B9 \/ {c9} c= B ; :: thesis: g . (B9 \/ {c9}) = g9 . (B9 \/ {c9})

A17: c9 in B by A16, ZFMISC_1:137;

then A18: c9 in B \ B9 by A15, XBOOLE_0:def 5;

c9 in B \/ {c} by A17, XBOOLE_0:def 3;

then A19: c9 in (B \/ {c}) \ B9 by A15, XBOOLE_0:def 5;

B9 c= B by A16, XBOOLE_1:11;

then A20: B9 c= B \/ {c} by A13, XBOOLE_1:1;

A24: for B9 being Element of Fin C holds S

c in B \/ {c} by ZFMISC_1:136;

then c in (B \/ {c}) \ B by A3, XBOOLE_0:def 5;

hence F $$ ((B \/ {.c.}),f) = F . ((g . B),(f . c)) by A5, A9, A11, XBOOLE_1:7

.= F . ((F $$ (B,f)),(f . c)) by A5, A6, A24 ;

:: thesis: verum