set ER = EqRel S;
set B = S ~ A;
for a, b being Element of A holds
( (canHom S) . (a + b) = ((canHom S) . a) + ((canHom S) . b) & (canHom S) . (a * b) = ((canHom S) . a) * ((canHom S) . b) & (canHom S) . (1_ A) = 1_ (S ~ A) )
proof
let a,
b be
Element of
A;
( (canHom S) . (a + b) = ((canHom S) . a) + ((canHom S) . b) & (canHom S) . (a * b) = ((canHom S) . a) * ((canHom S) . b) & (canHom S) . (1_ A) = 1_ (S ~ A) )
reconsider a1 =
(frac1 S) . a,
b1 =
(frac1 S) . b,
ab1 =
(frac1 S) . (a + b),
ab2 =
(frac1 S) . (a * b),
E1 =
(frac1 S) . (1. A) as
Element of
Frac S ;
reconsider x =
Class (
(EqRel S),
a1),
y =
Class (
(EqRel S),
b1) as
Element of
(S ~ A) by Lm41;
A1:
(canHom S) . a = x
by Def7;
A2:
(canHom S) . b = y
by Def7;
then A3:
((canHom S) . a) + ((canHom S) . b) =
Class (
(EqRel S),
((frac1 S) . (a + b)))
by A1, Lm37
.=
(canHom S) . (a + b)
by Def7
;
A4:
((canHom S) . a) * ((canHom S) . b) =
Class (
(EqRel S),
((frac1 S) . (a * b)))
by A1, A2, Lm39
.=
(canHom S) . (a * b)
by Def7
;
(canHom S) . (1. A) =
Class (
(EqRel S),
((frac1 S) . (1. A)))
by Def7
.=
1. (S ~ A)
by Lm43
;
hence
(
(canHom S) . (a + b) = ((canHom S) . a) + ((canHom S) . b) &
(canHom S) . (a * b) = ((canHom S) . a) * ((canHom S) . b) &
(canHom S) . (1_ A) = 1_ (S ~ A) )
by A3, A4;
verum
end;
hence
( canHom S is additive & canHom S is multiplicative & canHom S is unity-preserving )
; verum