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

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