let G, H be Ring; :: thesis: for F being Morphism of G,H st G <= H holds
ex f being Function of G,H st
( F = RingMorphismStr(# G,H,f #) & f is linear )
let F be Morphism of G,H; :: thesis: ( G <= H implies ex f being Function of G,H st
( F = RingMorphismStr(# G,H,f #) & f is linear ) )
assume A1: G <= H ; :: thesis: ex f being Function of G,H st
( F = RingMorphismStr(# G,H,f #) & f is linear )
A2: the Dom of F = dom F
.= G by A1, Def9 ;
A3: the Cod of F = cod F
.= H by A1, Def9 ;
then reconsider f = the Fun of F as Function of G,H by A2;
take f ; :: thesis: ( F = RingMorphismStr(# G,H,f #) & f is linear )
thus ( F = RingMorphismStr(# G,H,f #) & f is linear ) by A2, A3, Lm3; :: thesis: verum