set f = canHom_Z/ (p,F);
hereby VECTSP_1:def 19 canHom_Z/ (p,F) is multiplicative
let x,
y be
Element of
(Z/ p);
((canHom_Z/ (p,F)) . x) + ((canHom_Z/ (p,F)) . y) = (canHom_Z/ (p,F)) . (x + y)reconsider x1 =
x,
y1 =
y as
Element of
INT.Ring by ORDINAL1:def 12, NUMBERS:17;
A1:
x + y = (x1 + y1) mod p
by GR_CY_1:def 4;
reconsider z =
(x1 + y1) mod p as
Element of
INT.Ring by INT_1:def 2;
thus ((canHom_Z/ (p,F)) . x) + ((canHom_Z/ (p,F)) . y) =
(x1 '*' (1. F)) + ((canHom_Z/ (p,F)) . y)
by Lm14
.=
(x1 '*' (1. F)) + (y1 '*' (1. F))
by Lm14
.=
(x1 + y1) '*' (1. F)
by Th61
.=
z '*' (1. F)
by Th104
.=
(canHom_Z/ (p,F)) . (x + y)
by Lm14, A1
;
verum
end;
hereby GROUP_6:def 6 verum
let x,
y be
Element of
(Z/ p);
((canHom_Z/ (p,F)) . x) * ((canHom_Z/ (p,F)) . y) = (canHom_Z/ (p,F)) . (x * y)reconsider x1 =
x,
y1 =
y as
Element of
INT.Ring by ORDINAL1:def 12, NUMBERS:17;
A2:
x * y = (x1 * y1) mod p
by INT_3:def 10;
reconsider z =
(x1 * y1) mod p as
Element of
INT.Ring by INT_1:def 2;
thus ((canHom_Z/ (p,F)) . x) * ((canHom_Z/ (p,F)) . y) =
(x1 '*' (1. F)) * ((canHom_Z/ (p,F)) . y)
by Lm14
.=
(x1 '*' (1. F)) * (y1 '*' (1. F))
by Lm14
.=
(x1 * y1) '*' (1. F)
by Th66
.=
z '*' (1. F)
by Th104
.=
(canHom_Z/ (p,F)) . (x * y)
by Lm14, A2
;
verum
end;