theorem Th34: :: CIRCCMB3:34

for f being Function
for x1, x2, x3, x4, x5 being set st x1 in dom f & x2 in dom f & x3 in dom f & x4 in dom f & x5 in dom f holds
f * <*x1,x2,x3,x4,x5*> = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*>