set K = Image f;

now :: thesis: for x being Element of (Image f) st x <> 0. (Image f) holds
ex z being Element of (Image f) st z * x = 1. (Image f)

let x be Element of (Image f); :: thesis: ( x <> 0. (Image f) implies ex z being Element of (Image f) st z * x = 1. (Image f) )
assume A1: x <> 0. (Image f) ; :: thesis: ex z being Element of (Image f) st z * x = 1. (Image f)
A2: the carrier of (Image f) = rng f by RING_2:def 6;
consider y being object such that
A3: ( y in dom f & x = f . y ) by A2, FUNCT_1:def 3;
reconsider y = y as Element of F by A3;

now :: thesis: not y = 0. F

assume y = 0. F ; :: thesis: contradiction
then f . y = 0. R by RING_2:6
.= 0. (Image f) by RING_2:def 6 ;
hence contradiction by A3, A1; :: thesis: verum

end;

then consider a being Element of F such that
A4: a * y = 1. F by VECTSP_1:def 9;
reconsider b = f . a as Element of (Image f) by A2, FUNCT_2:4;
1. (Image f) = 1_ R by RING_2:def 6
.= f . (1_ F) by GROUP_1:def 13
.= (f . a) * (f . y) by A4, GROUP_6:def 6
.= ( the multF of R || (rng f)) . (b,x) by Th1, A2, A3
.= b * x by RING_2:def 6 ;
hence ex z being Element of (Image f) st z * x = 1. (Image f) ; :: thesis: verum

end;

hence Image f is almost_left_invertible ; :: thesis: verum