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)

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

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:40;
hence F . (F $$ B,f),(f . c) = f . c by A2, A4, SETWISEO:23
.= F $$ (B \/ {.c.}),f by A1, A4, SETWISEO:26 ;
:: thesis: verum

end;

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

consider g being Function of (Fin C),D such that
A6: 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
A7: for c' being Element of C holds g . {c'} = f . c' and
A8: for B' being Element of Fin C st B' c= B \/ {c} & B' <> {} holds
for c' being Element of C st c' in (B \/ {c}) \ B' holds
g . (B' \/ {c'}) = F . (g . B'),(f . c') by A1, SETWISEO:def 3;
consider g' being Function of (Fin C),D such that
A9: F $$ B,f = g' . B and
for e being Element of D st e is_a_unity_wrt F holds
g' . {} = e and
A10: for c' being Element of C holds g' . {c'} = f . c' and
A11: for B' being Element of Fin C st B' c= B & B' <> {} holds
for c' being Element of C st c' in B \ B' holds
g' . (B' \/ {c'}) = F . (g' . B'),(f . c') by A1, A2, SETWISEO:def 3;
defpred S₁[ set ] means ( $1 <> {} & $1 c= B implies g . $1 = g' . $1 );
A12: S₁[ {}. C] ;
A13: 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
A14: ( B' <> {} & B' c= B implies g . B' = g' . B' ) and
A15: not c' in B' and
B' \/ {c'} <> {} and
A16: B' \/ {c'} c= B ; :: thesis: g . (B' \/ {c'}) = g' . (B' \/ {c'})
A17: c' in B by A16, SETWISEO:8;
then A18: ( B' c= B & c' in B \ B' ) by A15, A16, XBOOLE_0:def 5, XBOOLE_1:11;
B c= B \/ {c} by XBOOLE_1:7;
then A19: B' c= B \/ {c} by A18, XBOOLE_1:1;
c' in B \/ {c} by A17, XBOOLE_0:def 3;
then A20: c' in (B \/ {c}) \ B' by A15, XBOOLE_0:def 5;

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

suppose B' = {} ; :: thesis: g . (B' \/ {c'}) = g' . (B' \/ {c'})

then ( g . (B' \/ {c'}) = f . c' & g' . (B' \/ {c'}) = f . c' ) by A7, A10;
hence g . (B' \/ {c'}) = g' . (B' \/ {c'}) ; :: thesis: verum

end;

suppose A21: B' <> {} ; :: thesis: g . (B' \/ {c'}) = g' . (B' \/ {c'})

hence g . (B' \/ {c'}) = F . (g' . B'),(f . c') by A8, A14, A16, A19, A20, XBOOLE_1:11
.= g' . (B' \/ {c'}) by A11, A18, A21 ;
:: thesis: verum

end;

end;

end;

A22: for B' being Element of Fin C holds S₁[B'] from SETWISEO:sch 2(A12, A13);
c in B \/ {c} by SETWISEO:6;
then ( B c= B \/ {c} & c in (B \/ {c}) \ B ) by A3, XBOOLE_0:def 5, XBOOLE_1:7;
hence F $$ (B \/ {.c.}),f = F . (g . B),(f . c) by A5, A6, A8
.= F . (F $$ B,f),(f . c) by A5, A9, A22 ;
:: thesis: verum

end;

end;