set g = canHom_Int R;
now :: thesis: for x, y being Element of INT.Ring holds (canHom_Int R) . (x + y) = ((canHom_Int R) . x) + ((canHom_Int R) . y)
let x, y be Element of INT.Ring; :: thesis: (canHom_Int R) . (x + y) = ((canHom_Int R) . x) + ((canHom_Int R) . y)
thus (canHom_Int R) . (x + y) = (x + y) '*' (1. R) by Def8
.= (x '*' (1. R)) + (y '*' (1. R)) by Th61
.= ((canHom_Int R) . x) + (y '*' (1. R)) by Def8
.= ((canHom_Int R) . x) + ((canHom_Int R) . y) by Def8 ; :: thesis: verum
end;
hence canHom_Int R is additive ; :: thesis: ( canHom_Int R is multiplicative & canHom_Int R is unity-preserving )
now :: thesis: for x, y being Element of INT.Ring holds (canHom_Int R) . (x * y) = ((canHom_Int R) . x) * ((canHom_Int R) . y)
let x, y be Element of INT.Ring; :: thesis: (canHom_Int R) . (x * y) = ((canHom_Int R) . x) * ((canHom_Int R) . y)
reconsider x1 = x, y1 = y as Integer ;
thus (canHom_Int R) . (x * y) = (x * y) '*' (1. R) by Def8
.= (x1 '*' (1. R)) * (y1 '*' (1. R)) by Th66
.= ((canHom_Int R) . x) * (y '*' (1. R)) by Def8
.= ((canHom_Int R) . x) * ((canHom_Int R) . y) by Def8 ; :: thesis: verum
end;
hence canHom_Int R is multiplicative ; :: thesis: canHom_Int R is unity-preserving
(canHom_Int R) . (1_ INT.Ring) = 1 '*' (1. R) by Def8
.= 1_ R by Th59 ;
hence canHom_Int R is unity-preserving ; :: thesis: verum