theorem :: GROUP_9:62

for O, E being set holds [:O,{(id E)}:] is Action of O,E by Lm1;