let R be Ring; :: thesis: for f being Homomorphism of INT.Ring,R holds f = canHom_Int R
let f be Homomorphism of INT.Ring,R; :: thesis: f = canHom_Int R
set g = canHom_Int R;
A1: dom f = the carrier of INT.Ring by FUNCT_2:def 1
.= dom (canHom_Int R) by FUNCT_2:def 1 ;
defpred S1[ Integer] means for j being Integer st j = $1 holds
f . j = j '*' (1. R);
now :: thesis: for j being Integer st j = 0 holds
f . j = j '*' (1. R)
let j be Integer; :: thesis: ( j = 0 implies f . j = j '*' (1. R) )
assume A2: j = 0 ; :: thesis: f . j = j '*' (1. R)
hence f . j = f . (0. INT.Ring)
.= 0. R by RING_2:6
.= j '*' (1. R) by A2, Th58 ;
:: thesis: verum
end;
then A3: S1[ 0 ] ;
A4: for u being Integer st S1[u] holds
( S1[u - 1] & S1[u + 1] )
proof
let u be Integer; :: thesis: ( S1[u] implies ( S1[u - 1] & S1[u + 1] ) )
assume A5: S1[u] ; :: thesis: ( S1[u - 1] & S1[u + 1] )
reconsider uu = u as Element of INT.Ring by INT_1:def 2;
now :: thesis: for k being Integer st k = u - 1 holds
f . k = k '*' (1. R)
let k be Integer; :: thesis: ( k = u - 1 implies f . k = k '*' (1. R) )
assume A6: k = u - 1 ; :: thesis: f . k = k '*' (1. R)
then k = uu - (1. INT.Ring) ;
hence f . k = (f . uu) - (f . (1. INT.Ring)) by RING_2:8
.= (uu '*' (1. R)) - (f . (1_ INT.Ring)) by A5
.= (uu '*' (1. R)) - (1_ R) by GROUP_1:def 13
.= (uu '*' (1. R)) - (1 '*' (1. R)) by Th59
.= k '*' (1. R) by Th63, A6 ;
:: thesis: verum
end;
hence S1[u - 1] ; :: thesis: S1[u + 1]
now :: thesis: for k being Integer st k = u + 1 holds
f . k = k '*' (1. R)
let k be Integer; :: thesis: ( k = u + 1 implies f . k = k '*' (1. R) )
assume A7: k = u + 1 ; :: thesis: f . k = k '*' (1. R)
then k = uu + (1. INT.Ring) ;
hence f . k = (f . uu) + (f . (1. INT.Ring)) by VECTSP_1:def 20
.= (uu '*' (1. R)) + (f . (1_ INT.Ring)) by A5
.= (uu '*' (1. R)) + (1_ R) by GROUP_1:def 13
.= (uu '*' (1. R)) + (1 '*' (1. R)) by Th59
.= k '*' (1. R) by Th61, A7 ;
:: thesis: verum
end;
hence S1[u + 1] ; :: thesis: verum
end;
A8: for i being Integer holds S1[i] from INT_1:sch 4(A3, A4);
now :: thesis: for x being object st x in dom f holds
f . x = (canHom_Int R) . x
let x be object ; :: thesis: ( x in dom f implies f . x = (canHom_Int R) . x )
assume x in dom f ; :: thesis: f . x = (canHom_Int R) . x
then reconsider a = x as Element of INT.Ring ;
reconsider aa = a as Integer ;
f . a = aa '*' (1. R) by A8;
hence f . x = (canHom_Int R) . x by Def8; :: thesis: verum
end;
hence f = canHom_Int R by A1; :: thesis: verum