let y, x be Element of R; :: thesis: ( x in { (a * i) where i is Element of R : i in I } implies x * y in { (a * i) where i is Element of R : i in I } )
assume x in { (a * i) where i is Element of R : i in I } ; :: thesis: x * y in { (a * i) where i is Element of R : i in I }
then consider i being Element of R such that
A1: ( x = a * i & i in I ) ;
( x * y = a * (i * y) & i * y in I ) by A1, Def3, GROUP_1:def 3;
hence x * y in { (a * i) where i is Element of R : i in I } ; :: thesis: verum