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 ) ;
assume f | B = f9 | B ; :: thesis: F $$ (B,f) = F $$ (B,f9)
then f | B = f9 * (id B) by RELAT_1:65;
hence F $$ (B,f) = F $$ (B,f9) by A1, A2, Th5; :: thesis: verum