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 ;
hence F . ((F \$\$ (B,f)),(f . c)) = f . c by
.= F \$\$ ((B \/ {.c.}),f) by ;
:: thesis: verum
end;
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 ;
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 ;
defpred S1[ 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 S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
proof
A13: B c= B \/ {c} by XBOOLE_1:7;
let B9 be Element of Fin C; :: thesis: for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]

let c9 be Element of C; :: thesis: ( S1[B9] & not c9 in B9 implies S1[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 ;
then A18: c9 in B \ B9 by ;
c9 in B \/ {c} by ;
then A19: c9 in (B \/ {c}) \ B9 by ;
B9 c= B by ;
then A20: B9 c= B \/ {c} by ;
per cases ( B9 = {} or B9 <> {} ) ;
suppose A21: B9 = {} ; :: thesis: g . (B9 \/ {c9}) = g9 . (B9 \/ {c9})
then g . (B9 \/ {c9}) = f . c9 by A10;
hence g . (B9 \/ {c9}) = g9 . (B9 \/ {c9}) by ; :: thesis: verum
end;
suppose A22: B9 <> {} ; :: thesis: g . (B9 \/ {c9}) = g9 . (B9 \/ {c9})
hence g . (B9 \/ {c9}) = F . ((g9 . B9),(f . c9)) by
.= g9 . (B9 \/ {c9}) by ;
:: thesis: verum
end;
end;
end;
A23: S1[ {}. C] ;
A24: for B9 being Element of Fin C holds S1[B9] from c in B \/ {c} by ZFMISC_1:136;
then c in (B \/ {c}) \ B by ;
hence F \$\$ ((B \/ {.c.}),f) = F . ((g . B),(f . c)) by
.= F . ((F \$\$ (B,f)),(f . c)) by A5, A6, A24 ;
:: thesis: verum
end;
end;