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

now :: thesis: for a being Element of (embField f) holds a is right_complementable

let a be Element of (embField f); :: thesis: b₁ is right_complementable
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 right_complementable

then reconsider a1 = a as Element of K ;
a1 is right_complementable ;
then consider b1 being Element of K such that
B1: a1 + b1 = 0. K ;
reconsider y = b1 as Element of carr f by XBOOLE_0:def 3;
reconsider b = y as Element of (embField f) by defemb;
a + b = a1 + b1 by Lm7
.= 0. (embField f) by B1, defemb ;
hence a is right_complementable ; :: thesis: verum

end;

suppose A2: not x in [#] K ; :: thesis: b₁ is right_complementable

then reconsider a1 = a as Element of T by Lm1;
a1 is right_complementable ;
then consider b1 being Element of T such that
B2: a1 + b1 = 0. T ;
( dom f = [#] K & the addF of T . (a1,b1) = f . (0. K) ) by B2, RING_2:6, FUNCT_2:def 1;
then D0: the addF of T . (a1,b1) in rng f by FUNCT_1:3;
then D1: not the addF of T . (a1,b1) in ([#] T) \ (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 right_complementable

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;
C2: [#] (embField f) = carr f by defemb;
then the addF of T . (a1,(f . bx)) in [#] K by Lm2, A2, D1, C1;
hence a is right_complementable by Lm2, A2, D1, C1, C2; :: thesis: verum

end;

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

then b1 in ([#] T) \ (rng f) by XBOOLE_0:def 5;
then reconsider y = b1 as Element of carr f by XBOOLE_0:def 3;
reconsider b = y as Element of (embField f) by defemb;
E1: not b in [#] K by AS, XBOOLE_0:def 4;
Y1: ( dom f = [#] K & f . (0. K) = 0. T ) by RING_2:6, FUNCT_2:def 1;
a + b = (f ") . (0. T) by A2, B2, D0, E1, Lm9
.= 0. K by Y1, FUNCT_1:32
.= 0. (embField f) by defemb ;
hence a is right_complementable ; :: thesis: verum

end;

end;

end;

end;

end;

hence embField f is right_complementable ; :: thesis: verum