let M, N be non empty multMagma ; :: thesis: for f being Function of M,N st f is multiplicative holds
equ_kernel f is compatible
let f be Function of M,N; :: thesis: ( f is multiplicative implies equ_kernel f is compatible )
assume A1: f is multiplicative ; :: thesis: equ_kernel f is compatible
set R = equ_kernel f;
for v, v9, w, w9 being Element of M st v in Class ((equ_kernel f),v9) & w in Class ((equ_kernel f),w9) holds
v * w in Class ((equ_kernel f),(v9 * w9))

proof

let v, v9, w, w9 be Element of M; :: thesis: ( v in Class ((equ_kernel f),v9) & w in Class ((equ_kernel f),w9) implies v * w in Class ((equ_kernel f),(v9 * w9)) )
assume v in Class ((equ_kernel f),v9) ; :: thesis: ( not w in Class ((equ_kernel f),w9) or v * w in Class ((equ_kernel f),(v9 * w9)) )
then A2: [v9,v] in equ_kernel f by EQREL_1:18;
assume w in Class ((equ_kernel f),w9) ; :: thesis: v * w in Class ((equ_kernel f),(v9 * w9))
then [w9,w] in equ_kernel f by EQREL_1:18;
then A3: f . w9 = f . w by Def8;
f . (v9 * w9) = (f . v9) * (f . w9) by A1, GROUP_6:def 6
.= (f . v) * (f . w) by A2, A3, Def8
.= f . (v * w) by A1, GROUP_6:def 6 ;
then [(v9 * w9),(v * w)] in equ_kernel f by Def8;
hence v * w in Class ((equ_kernel f),(v9 * w9)) by EQREL_1:18; :: thesis: verum

end;

hence equ_kernel f is compatible ; :: thesis: verum