theorem Th11: :: NAT_3:11

for a being Nat holds (<*> REAL) |^ a = <*> REAL