let K be Field; :: thesis: for F being K -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
embField f is almost_left_invertible
let F be K -monomorphic Field; :: thesis: for f being Monomorphism of K,F st K,F are_disjoint holds
embField f is almost_left_invertible
let f be Monomorphism of K,F; :: thesis: ( K,F are_disjoint implies embField f is almost_left_invertible )
assume AS: K,F are_disjoint ; :: thesis: embField f is almost_left_invertible

now :: thesis: for a being Element of (embField f) st a <> 0. (embField f) holds
a is left_invertible

let a be Element of (embField f); :: thesis: ( a <> 0. (embField f) implies b₁ is left_invertible )
assume a <> 0. (embField f) ; :: thesis: b₁ is left_invertible
then X: a <> 0. K by defemb;
reconsider x = a as Element of carr f by defemb;

per cases ( x in [#] K or not x in [#] K ) ;

suppose x in [#] K ; :: thesis: b₁ is left_invertible

then reconsider a1 = a as Element of K ;
a1 is left_invertible by X, ALGSTR_0:def 39;
then consider b1 being Element of K such that
B: b1 * a1 = 1. K ;
reconsider y = b1 as Element of carr f by XBOOLE_0:def 3;
reconsider b = y as Element of (embField f) by defemb;
b * a = a * b by GROUP_1:def 12
.= a1 * b1 by Lm11
.= b1 * a1 by GROUP_1:def 12
.= 1. (embField f) by B, defemb ;
hence a is left_invertible ; :: thesis: verum

end;

suppose A: not x in [#] K ; :: thesis: b₁ is left_invertible

then X: ( x in [#] F & not x in rng f ) by Lm1;
reconsider a1 = a as Element of F by A, Lm1;
Z: dom f = [#] K by FUNCT_2:def 1;
f . (0. K) = 0. F by RING_2:6;
then 0. F in rng f by Z, FUNCT_1:def 3;
then a1 is left_invertible by X, ALGSTR_0:def 39;
then consider b1 being Element of F such that
B: b1 * a1 = 1. F ;
U: ( b1 <> 0. F & a1 <> 0. F ) by B;
the multF of F . (a1,b1) = a1 * b1
.= 1_ F by B, GROUP_1:def 12
.= f . (1_ K) by GROUP_1:def 13 ;
then D: the multF of F . (a1,b1) in rng f by Z, FUNCT_1:3;
then D1: not the multF of F . (a1,b1) in ([#] F) \ (rng f) by XBOOLE_0:def 5;

per cases ( b1 in rng f or not b1 in rng f ) ;

suppose b1 in rng f ; :: thesis: b₁ is left_invertible

then consider b1r being object such that
C1: ( b1r in dom f & f . b1r = b1 ) by FUNCT_1:def 3;
reconsider b1r = b1r as Element of K by C1;
[#] (embField f) = carr f by defemb;
then reconsider bx = b1r as Element of (embField f) by XBOOLE_0:def 3;
reconsider y = bx as Element of carr f by defemb;
C4: bx <> 0. K by U, C1, RING_2:6;
[#] (embField f) = carr f by defemb;
hence a is left_invertible by Lm4, A, D1, C1, C4; :: thesis: verum

end;

suppose not b1 in rng f ; :: thesis: b₁ is left_invertible

then b1 in ([#] F) \ (rng f) by XBOOLE_0:def 5;
then b1 is Element of carr f by XBOOLE_0:def 3;
then reconsider b = b1 as Element of (embField f) by defemb;
E: not b in [#] K by AS, XBOOLE_0:def 4;
b * a = a * b by GROUP_1:def 12
.= (f ") . (a1 * b1) by A, D, E, Lm13
.= (f ") . (1_ F) by B, GROUP_1:def 12
.= 1. K by Th3
.= 1. (embField f) by defemb ;
hence a is left_invertible ; :: thesis: verum

end;

end;

end;

end;

end;

hence embField f is almost_left_invertible ; :: thesis: verum