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:83, RELAT_1:115;
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:62;
f | B is one-to-one by A2, FUNCT_1:52;
hence H $$ ((f .: B),h) = H $$ (B,(h * f)) by A1, A4, A3, Th5; :: thesis: verum