theorem Th33: :: CIRCCMB3:33

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