let p be Prime; :: thesis: for F being Z/ p -homomorphic p -characteristic Field
for f being Homomorphism of (Z/ p),F holds f = canHom_Z/ (p,F)
let F be Z/ p -homomorphic p -characteristic Field; :: thesis: for f being Homomorphism of (Z/ p),F holds f = canHom_Z/ (p,F)
let f be Homomorphism of (Z/ p),F; :: thesis: f = canHom_Z/ (p,F)
set g = canHom_Z/ (p,F);
A1: f is unity-preserving ;
A2: ( canHom_Z/ (p,F) is unity-preserving & canHom_Z/ (p,F) is additive & canHom_Z/ (p,F) is multiplicative ) ;
A3: dom f = the carrier of (Z/ p) by FUNCT_2:def 1
.= dom (canHom_Z/ (p,F)) by FUNCT_2:def 1 ;
A4: 1. (Z/ p) = 1 by INT_3:14, INT_2:def 4;
reconsider p1 = p - 1 as Element of NAT by INT_1:3;
A5: p1 + 1 = p ;
defpred S₁[ Nat] means for j being Element of (Z/ p) st j = $1 holds
f . j = (canHom_Z/ (p,F)) . j;
f . 0 = f . (0. (Z/ p)) by NAT_1:44, SUBSET_1:def 8
.= 0. F by RING_2:6
.= (canHom_Z/ (p,F)) . (0. (Z/ p)) by RING_2:6
.= (canHom_Z/ (p,F)) . 0 by NAT_1:44, SUBSET_1:def 8 ;
then A6: S₁[ 0 ] ;
A7: for k being Element of NAT st 0 <= k & k < p1 & S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( 0 <= k & k < p1 & S₁[k] implies S₁[k + 1] )
assume A8: ( 0 <= k & k < p1 ) ; :: thesis: ( not S₁[k] or S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]
reconsider e = 1 as Element of Segm p by A4;
k < p by A5, A8, NAT_1:13;
then reconsider z = k as Element of (Z/ p) by NAT_1:44;
reconsider z0 = z as Element of Segm p ;
A10: k + 1 < p1 + 1 by A8, XREAL_1:6;
then reconsider z1 = k + 1 as Element of Segm p by NAT_1:44;
reconsider z1 = z1 as Element of (Z/ p) ;
A11: z + (1. (Z/ p)) = (addint p) . (k,1) by INT_3:14, INT_2:def 4
.= z0 + e by A10, INT_3:7
.= k + 1 ;
f . z1 = (f . z) + (f . (1. (Z/ p))) by A11, VECTSP_1:def 20
.= ((canHom_Z/ (p,F)) . z) + ((canHom_Z/ (p,F)) . (1. (Z/ p))) by A9, A1, A2
.= (canHom_Z/ (p,F)) . z1 by A11, A2 ;
hence S₁[k + 1] ; :: thesis: verum

end;

A12: for k being Element of NAT st 0 <= k & k <= p1 holds
S₁[k] from INT_1:sch 7(A6, A7);

now :: thesis: for x being object st x in dom f holds
f . x = (canHom_Z/ (p,F)) . x

let x be object ; :: thesis: ( x in dom f implies f . x = (canHom_Z/ (p,F)) . x )
assume x in dom f ; :: thesis: f . x = (canHom_Z/ (p,F)) . x
then reconsider a = x as Element of Segm p ;
a < p1 + 1 by NAT_1:44;
then a <= p - 1 by NAT_1:13;
hence f . x = (canHom_Z/ (p,F)) . x by A12; :: thesis: verum

end;

hence f = canHom_Z/ (p,F) by A3; :: thesis: verum