let F be F_Rat -homomorphic 0 -characteristic Field; :: thesis: for f being Homomorphism of F_Rat,F holds f = canHom_Rat F
let f be Homomorphism of F_Rat,F; :: thesis: f = canHom_Rat F
set g = canHom_Rat F;
A1: f is unity-preserving ;
A2: f is multiplicative ;
A3: canHom_Rat F is unity-preserving ;
A4: dom f = the carrier of F_Rat by FUNCT_2:def 1
.= dom (canHom_Rat F) by FUNCT_2:def 1 ;
defpred S1[ Integer] means for j being Element of F_Rat st j = $1 holds
f . j = (canHom_Rat F) . j;
A5: 0. F_Rat = 0 ;
then f . 0 = 0. F by RING_2:6
.= (canHom_Rat F) . 0 by A5, RING_2:6 ;
then A6: S1[ 0 ] ;
A7: now :: thesis: for u being Integer st S1[u] holds
( S1[u - 1] & S1[u + 1] )
let u be Integer; :: thesis: ( S1[u] implies ( S1[u - 1] & S1[u + 1] ) )
assume A8: S1[u] ; :: thesis: ( S1[u - 1] & S1[u + 1] )
reconsider uu = u as Element of F_Rat by RAT_1:def 2;
now :: thesis: for k being Integer st k = u - 1 holds
f . k = (canHom_Rat F) . k
let k be Integer; :: thesis: ( k = u - 1 implies f . k = (canHom_Rat F) . k )
assume k = u - 1 ; :: thesis: f . k = (canHom_Rat F) . k
then A9: k = uu - (1. F_Rat) ;
hence f . k = (f . uu) - (f . (1. F_Rat)) by RING_2:8
.= ((canHom_Rat F) . uu) - ((canHom_Rat F) . (1_ F_Rat)) by A8, A1, A3
.= (canHom_Rat F) . k by A9, RING_2:8 ;
:: thesis: verum
end;
hence S1[u - 1] ; :: thesis: S1[u + 1]
now :: thesis: for k being Integer st k = u + 1 holds
f . k = (canHom_Rat F) . k
let k be Integer; :: thesis: ( k = u + 1 implies f . k = (canHom_Rat F) . k )
assume k = u + 1 ; :: thesis: f . k = (canHom_Rat F) . k
then A10: k = uu + (1. F_Rat) ;
hence f . k = (f . uu) + (f . (1. F_Rat)) by VECTSP_1:def 20
.= ((canHom_Rat F) . uu) + ((canHom_Rat F) . (1_ F_Rat)) by A8, A1, A3
.= (canHom_Rat F) . k by A10, VECTSP_1:def 20 ;
:: thesis: verum
end;
hence S1[u + 1] ; :: thesis: verum
end;
A11: for i being Integer holds S1[i] from INT_1:sch 4(A6, A7);
 A12: for i being Integer
for j being Element of F_Rat st j = i holds
f . j = (canHom_Int F) . i
proof
let i be Integer; :: thesis: for j being Element of F_Rat st j = i holds
f . j = (canHom_Int F) . i
let j be Element of F_Rat; :: thesis: ( j = i implies f . j = (canHom_Int F) . i )
assume A13: j = i ; :: thesis: f . j = (canHom_Int F) . i
A14: canHom_Int F = (canHom_Rat F) | INT by Th97;
thus f . j = (canHom_Rat F) . i by A13, A11
.= (canHom_Int F) . i by A14, INT_1:def 2, FUNCT_1:49 ; :: thesis: verum
end;
now :: thesis: for x being object st x in dom f holds
f . x = (canHom_Rat F) . x
let x be object ; :: thesis: ( x in dom f implies f . x = (canHom_Rat F) . x )
assume x in dom f ; :: thesis: f . x = (canHom_Rat F) . x
then reconsider a = x as Element of F_Rat ;
reconsider a1 = numerator a as Element of F_Rat by RAT_1:def 2;
reconsider a2 = denominator a as Element of F_Rat by RAT_1:def 2;
A15: a2 <> 0. F_Rat ;
(canHom_Rat F) . a = ((canHom_Int F) . (numerator a)) / ((canHom_Int F) . (denominator a)) by Def11
.= (f . a1) / ((canHom_Int F) . (denominator a)) by A12
.= (f . a1) / (f . a2) by A12
.= (f . a1) * (f . (a2 ")) by A15, QUOFIELD:52
.= f . (a1 * (a2 ")) by A2
.= f . ((numerator a) * ((denominator a) ")) by GAUSSINT:15
.= f . a by RAT_1:15 ;
hence f . x = (canHom_Rat F) . x ; :: thesis: verum
end;
hence f = canHom_Rat F by A4; :: thesis: verum