let M, N 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 M : f . v = g . v } is stable Subset of M
let f, g be Function of M,N; :: thesis: ( f is multiplicative & g is multiplicative implies { v where v is Element of M : f . v = g . v } is stable Subset of M )
assume A1: f is multiplicative ; :: thesis: ( not g is multiplicative or { v where v is Element of M : f . v = g . v } is stable Subset of M )
assume A2: g is multiplicative ; :: thesis: { v where v is Element of M : f . v = g . v } is stable Subset of M
set X = { v where v is Element of M : f . v = g . v } ;
for x being object st x in { v where v is Element of M : f . v = g . v } holds
x in the carrier of M

proof

let x be object ; :: thesis: ( x in { v where v is Element of M : f . v = g . v } implies x in the carrier of M )
assume x in { v where v is Element of M : f . v = g . v } ; :: thesis: x in the carrier of M
then consider v being Element of M 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 M : f . v = g . v } as Subset of M by TARSKI:def 3;
for v, w being Element of M st v in X & w in X holds
v * w in X

proof

let v, w be Element of M; :: 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 v9 being Element of M such that
A4: ( v = v9 & f . v9 = g . v9 ) ;
assume w in X ; :: thesis: v * w in X
then consider w9 being Element of M such that
A5: ( w = w9 & f . w9 = g . w9 ) ;
f . (v * w) = (g . v) * (g . w) by A4, A5, A1, GROUP_6:def 6
.= g . (v * w) by A2, GROUP_6:def 6 ;
hence v * w in X ; :: thesis: verum

end;

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