let C, D be non empty set ; :: thesis: for B being Element of Fin C
for F being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & f | B = f9 | B holds
F $$ B,f = F $$ B,f9
let B be Element of Fin C; :: thesis: for F being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & f | B = f9 | B holds
F $$ B,f = F $$ B,f9
let F be BinOp of D; :: thesis: for f, f9 being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & f | B = f9 | B holds
F $$ B,f = F $$ B,f9
let f, f9 be Function of C,D; :: thesis: ( F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & f | B = f9 | B implies F $$ B,f = F $$ B,f9 )
assume A1: ( F is commutative & F is associative & ( B <> {} or F is having_a_unity ) ) ; :: thesis: ( not f | B = f9 | B or F $$ B,f = F $$ B,f9 )
set s = id B;
A2: ( dom (id B) = B & rng (id B) = B ) by RELAT_1:71;
assume f | B = f9 | B ; :: thesis: F $$ B,f = F $$ B,f9
then f | B = f9 * (id B) by RELAT_1:94;
hence F $$ B,f = F $$ B,f9 by A1, A2, Th7; :: thesis: verum