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

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