let p be Prime; :: thesis: for F being Field
for x being Element of (Z/ p)
for y being Element of INT.Ring st x = y holds
(canHom_Z/ (p,F)) . x = y '*' (1. F)
let F be Field; :: thesis: for x being Element of (Z/ p)
for y being Element of INT.Ring st x = y holds
(canHom_Z/ (p,F)) . x = y '*' (1. F)
let x be Element of (Z/ p); :: thesis: for y being Element of INT.Ring st x = y holds
(canHom_Z/ (p,F)) . x = y '*' (1. F)
let y be Element of INT.Ring; :: thesis: ( x = y implies (canHom_Z/ (p,F)) . x = y '*' (1. F) )
assume x = y ; :: thesis: (canHom_Z/ (p,F)) . x = y '*' (1. F)
hence (canHom_Z/ (p,F)) . x = (canHom_Int F) . y by FUNCT_1:49
.= y '*' (1. F) by Def8 ;
:: thesis: verum