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

proof

let v, w be Element of N; :: 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 v9 being object such that
A2: ( v9 in dom f & v9 in X & v = f . v9 ) by FUNCT_1:def 6;
assume w in f .: X ; :: thesis: v * w in f .: X
then consider w9 being object such that
A3: ( w9 in dom f & w9 in X & w = f . w9 ) by FUNCT_1:def 6;
reconsider v9 = v9, w9 = w9 as Element of M by A2, A3;
v9 * w9 in the carrier of M ;
then A4: v9 * w9 in dom f by FUNCT_2:def 1;
v9 * w9 in X by A2, A3, Def10;
then f . (v9 * w9) in f .: X by A4, FUNCT_1:def 6;
hence v * w in f .: X by A2, A3, A1, GROUP_6:def 6; :: thesis: verum

end;

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