theorem Th64: :: HILB10_7:64

for D being non empty set
for A being BinOp of D st A is commutative & A is associative holds
for f, g being non empty FinSequence
for F being Function of (dom f),D
for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))