let A, B be non degenerated commutative Ring; :: thesis: for S being non empty multiplicatively-closed without_zero Subset of A
for f being Function of A,B
for s being Element of S st f is RingHomomorphism & f .: S c= Unit_Set B holds
f . s is Unit of B
let S be non empty multiplicatively-closed without_zero Subset of A; :: thesis: for f being Function of A,B
for s being Element of S st f is RingHomomorphism & f .: S c= Unit_Set B holds
f . s is Unit of B
let f be Function of A,B; :: thesis: for s being Element of S st f is RingHomomorphism & f .: S c= Unit_Set B holds
f . s is Unit of B
let s be Element of S; :: thesis: ( f is RingHomomorphism & f .: S c= Unit_Set B implies f . s is Unit of B )
assume A1: ( f is RingHomomorphism & f .: S c= Unit_Set B ) ; :: thesis: f . s is Unit of B
A2: dom f = the carrier of A by FUNCT_2:def 1;
reconsider t = f . s as object ;
t in f .: S by A2, FUNCT_1:def 6;
then 1. B = (f . s) * ((f . s) ["]) by A1, Def2;
then f . s divides 1. B ;
then f . s is unital ;
hence f . s is Unit of B ; :: thesis: verum