let K be Field; :: thesis: for F being K -monomorphic Field
for f being Monomorphism of K,F
for a being Element of K st a <> 0. K holds
f . (a ") = (f . a) "
let F be K -monomorphic Field; :: thesis: for f being Monomorphism of K,F
for a being Element of K st a <> 0. K holds
f . (a ") = (f . a) "
let f be Monomorphism of K,F; :: thesis: for a being Element of K st a <> 0. K holds
f . (a ") = (f . a) "
let x be Element of K; :: thesis: ( x <> 0. K implies f . (x ") = (f . x) " )
assume AS: x <> 0. K ; :: thesis: f . (x ") = (f . x) "
A1: (f . (x ")) * (f . x) = f . ((x ") * x) by GROUP_6:def 6
.= f . (1_ K) by AS, VECTSP_1:def 10
.= 1_ F by GROUP_1:def 13
.= 1. F ;
f . x <> 0. F by AS, Th4;
hence f . (x ") = (f . x) " by A1, VECTSP_1:def 10; :: thesis: verum