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

proof

let v, w be Element of M; :: thesis: ( v in f " Y & w in f " Y implies v * w in f " Y )
assume v in f " Y ; :: thesis: ( not w in f " Y or v * w in f " Y )
then A2: ( v in dom f & f . v in Y ) by FUNCT_1:def 7;
assume w in f " Y ; :: thesis: v * w in f " Y
then A3: ( w in dom f & f . w in Y ) by FUNCT_1:def 7;
v * w in the carrier of M ;
then A4: v * w in dom f by FUNCT_2:def 1;
(f . v) * (f . w) in Y by A2, A3, Def10;
then f . (v * w) in Y by A1, GROUP_6:def 6;
hence v * w in f " Y by A4, FUNCT_1:def 7; :: thesis: verum

end;

hence f " Y is stable Subset of M by Def10; :: thesis: verum