let C, D, E be non empty set ; :: thesis: for B being Element of Fin C
for f being Function of C,D
for H being BinOp of E
for h being Function of D,E st H is commutative & H is associative & ( B <> {} or H is having_a_unity ) & f is one-to-one holds
H $$ (f .: B),h = H $$ B,(h * f)
let B be Element of Fin C; :: thesis: for f being Function of C,D
for H being BinOp of E
for h being Function of D,E st H is commutative & H is associative & ( B <> {} or H is having_a_unity ) & f is one-to-one holds
H $$ (f .: B),h = H $$ B,(h * f)
let f be Function of C,D; :: thesis: for H being BinOp of E
for h being Function of D,E st H is commutative & H is associative & ( B <> {} or H is having_a_unity ) & f is one-to-one holds
H $$ (f .: B),h = H $$ B,(h * f)
let H be BinOp of E; :: thesis: for h being Function of D,E st H is commutative & H is associative & ( B <> {} or H is having_a_unity ) & f is one-to-one holds
H $$ (f .: B),h = H $$ B,(h * f)
let h be Function of D,E; :: thesis: ( H is commutative & H is associative & ( B <> {} or H is having_a_unity ) & f is one-to-one implies H $$ (f .: B),h = H $$ B,(h * f) )
assume that
A1: ( H is commutative & H is associative & ( B <> {} or H is having_a_unity ) ) and
A2: f is one-to-one ; :: thesis: H $$ (f .: B),h = H $$ B,(h * f)
set s = f | B;
A3: ( rng (f | B) = f .: B & (h * f) | B = h * (f | B) ) by RELAT_1:112, RELAT_1:148;
B c= C by FINSUB_1:def 5;
then B c= dom f by FUNCT_2:def 1;
then A4: dom (f | B) = B by RELAT_1:91;
f | B is one-to-one by A2, FUNCT_1:84;
hence H $$ (f .: B),h = H $$ B,(h * f) by A1, A4, A3, Th7; :: thesis: verum