theorem :: EUCLID_7:3

for z being set holds <*z*> * <*1*> = <*z*>