let C, D, E be non empty set ; 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; 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; 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; 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; ( 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
; 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; verum