let G, H be Ring; 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; ( G <= H implies ex f being Function of G,H st
( F = RingMorphismStr(# G,H,f #) & f is linear ) )
assume A1:
G <= H
; ex f being Function of G,H st
( F = RingMorphismStr(# G,H,f #) & f is linear )
A2: the Cod of F =
cod F
.=
H
by A1, Def8
;
A3: the Dom of F =
dom F
.=
G
by A1, Def8
;
then reconsider f = the Fun of F as Function of G,H by A2;
take
f
; ( F = RingMorphismStr(# G,H,f #) & f is linear )
thus
( F = RingMorphismStr(# G,H,f #) & f is linear )
by A3, A2, Lm3; verum