let F be strict RingMorphism; :: thesis: ex G, H being Ring ex f being Function of G,H st
( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
consider G, H being Ring such that
A1: G <= H and
dom F = G and
cod F = H and
A2: F is Morphism of G,H by Lm6;
reconsider F9 = F as Morphism of G,H by A2;
consider f being Function of G,H such that
A3: ( F9 = RingMorphismStr(# G,H,f #) & f is linear ) by A1, Lm7;
take G ; :: thesis: ex H being Ring ex f being Function of G,H st
( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
take H ; :: thesis: ex f being Function of G,H st
( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
take f ; :: thesis: ( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
thus ( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear ) by A3; :: thesis: verum