let K be F -isomorphic Ring; :: thesis: K is almost_left_invertible
set f = the Isomorphism of F,K;
reconsider g = the Isomorphism of F,K " as Isomorphism of K,F by Lm7;
A1: g " = the Isomorphism of F,K ;
now :: thesis: for x being Element of K st x <> 0. K holds
ex y being Element of K st y * x = 1. K
let x be Element of K; :: thesis: ( x <> 0. K implies ex y being Element of K st y * x = 1. K )
assume A2: x <> 0. K ; :: thesis: ex y being Element of K st y * x = 1. K
now :: thesis: not g . x = 0. F
assume g . x = 0. F ; :: thesis: contradiction
then g . x = g . (0. K) by RING_2:6;
hence contradiction by A2, FUNCT_2:19; :: thesis: verum
end;
then consider a being Element of F such that
A3: a * (g . x) = 1. F by VECTSP_1:def 9;
1. K = 1_ K
.= the Isomorphism of F,K . (1_ F) by GROUP_1:def 13
.= ( the Isomorphism of F,K . a) * ( the Isomorphism of F,K . (g . x)) by A3, GROUP_6:def 6
.= ( the Isomorphism of F,K . a) * x by A1, FUNCT_2:26 ;
hence ex y being Element of K st y * x = 1. K ; :: thesis: verum
end;
hence K is almost_left_invertible ; :: thesis: verum