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