let M, N be non empty multMagma ; :: thesis: for f being Function of M,N
for X being stable Subset of st f is multiplicative holds
f .: X is stable Subset of
let f be Function of M,N; :: thesis: for X being stable Subset of st f is multiplicative holds
f .: X is stable Subset of
let X be stable Subset of ; :: thesis: ( f is multiplicative implies f .: X is stable Subset of )
assume A1: f is multiplicative ; :: thesis: f .: X is stable Subset of
for v, w being Element of st v in f .: X & w in f .: X holds
v * w in f .: X

proof

let v, w be Element of ; :: thesis: ( v in f .: X & w in f .: X implies v * w in f .: X )
assume v in f .: X ; :: thesis: ( not w in f .: X or v * w in f .: X )
then consider v' being set such that
A2: ( v' in dom f & v' in X & v = f . v' ) by FUNCT_1:def 12;
assume w in f .: X ; :: thesis: v * w in f .: X
then consider w' being set such that
A3: ( w' in dom f & w' in X & w = f . w' ) by FUNCT_1:def 12;
reconsider v' = v', w' = w' as Element of by A2, A3;
v' * w' in the carrier of M ;
then A4: v' * w' in dom f by FUNCT_2:def 1;
v' * w' in X by A2, A3, Def11;
then f . (v' * w') in f .: X by A4, FUNCT_1:def 12;
hence v * w in f .: X by A2, A3, A1, GROUP_6:def 7; :: thesis: verum

end;

hence f .: X is stable Subset of by Def11; :: thesis: verum