let N, M be non empty multMagma ; :: thesis: for f, g being Function of M,N st f is multiplicative & g is multiplicative holds
{ v where v is Element of : f . v = g . v } is stable Subset of
let f, g be Function of M,N; :: thesis: ( f is multiplicative & g is multiplicative implies { v where v is Element of : f . v = g . v } is stable Subset of )
assume A1: f is multiplicative ; :: thesis: ( not g is multiplicative or { v where v is Element of : f . v = g . v } is stable Subset of )
assume A2: g is multiplicative ; :: thesis: { v where v is Element of : f . v = g . v } is stable Subset of
set X = { v where v is Element of : f . v = g . v } ;
for x being set st x in { v where v is Element of : f . v = g . v } holds
x in the carrier of M

proof

let x be set ; :: thesis: ( x in { v where v is Element of : f . v = g . v } implies x in the carrier of M )
assume x in { v where v is Element of : f . v = g . v } ; :: thesis: x in the carrier of M
then consider v being Element of such that
A3: ( x = v & f . v = g . v ) ;
thus x in the carrier of M by A3; :: thesis: verum

end;

then reconsider X = { v where v is Element of : f . v = g . v } as Subset of by TARSKI:def 3;
for v, w being Element of st v in X & w in X holds
v * w in X

proof

let v, w be Element of ; :: thesis: ( v in X & w in X implies v * w in X )
assume v in X ; :: thesis: ( not w in X or v * w in X )
then consider v' being Element of such that
A4: ( v = v' & f . v' = g . v' ) ;
assume w in X ; :: thesis: v * w in X
then consider w' being Element of such that
A5: ( w = w' & f . w' = g . w' ) ;
f . (v * w) = (g . v) * (g . w) by A4, A5, A1, GROUP_6:def 7
.= g . (v * w) by A2, GROUP_6:def 7 ;
hence v * w in X ; :: thesis: verum

end;

hence { v where v is Element of : f . v = g . v } is stable Subset of by Def11; :: thesis: verum