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, v', w, w' being Element of st v in Class (equ_kernel f),v' & w in Class (equ_kernel f),w' holds
v * w in Class (equ_kernel f),(v' * w')

proof

let v, v', w, w' be Element of ; :: thesis: ( v in Class (equ_kernel f),v' & w in Class (equ_kernel f),w' implies v * w in Class (equ_kernel f),(v' * w') )
assume v in Class (equ_kernel f),v' ; :: thesis: ( not w in Class (equ_kernel f),w' or v * w in Class (equ_kernel f),(v' * w') )
then A2: [v',v] in equ_kernel f by EQREL_1:26;
assume w in Class (equ_kernel f),w' ; :: thesis: v * w in Class (equ_kernel f),(v' * w')
then [w',w] in equ_kernel f by EQREL_1:26;
then A3: f . w' = f . w by Def9;
f . (v' * w') = (f . v') * (f . w') by A1, GROUP_6:def 7
.= (f . v) * (f . w) by A2, A3, Def9
.= f . (v * w) by A1, GROUP_6:def 7 ;
then [(v' * w'),(v * w)] in equ_kernel f by Def9;
hence v * w in Class (equ_kernel f),(v' * w') by EQREL_1:26; :: thesis: verum

end;

hence equ_kernel f is compatible by Def4; :: thesis: verum