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

for v, w being Element of M st v in X & w in X holds

v * w in X

{ 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

then reconsider X = { v where v is Element of M : f . v = g . v } as Subset of M by TARSKI:def 3;
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;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

for v, w being Element of M st v in X & w in X holds

v * w in X

proof

hence
{ v where v is Element of M : f . v = g . v } is stable Subset of M
by Def10; :: thesis: verum
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;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