set FE = F_Alg E;
A1: 0. (F_Alg E) = 0. E by d;
A2: the carrier of (F_Alg E) = Alg_El E by d;

hereby :: according to RLVECT_1:def 2 :: thesis: ( F_Alg E is add-associative & F_Alg E is right_zeroed & F_Alg E is right_complementable )

let x, y be Element of (F_Alg E); :: thesis: x + y = y + x
reconsider a = x, b = y as Element of E by Lm10;
thus x + y = a + b by Lm11
.= y + x by Lm11 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( F_Alg E is right_zeroed & F_Alg E is right_complementable )

let x, y, z be Element of (F_Alg E); :: thesis: (x + y) + z = x + (y + z)
reconsider a = x, b = y, c = z as Element of E by Lm10;
A3: y + z = b + c by Lm11;
x + y = a + b by Lm11;
hence (x + y) + z = (a + b) + c by Lm11
.= a + (b + c) by RLVECT_1:def 3
.= x + (y + z) by A3, Lm11 ;
:: thesis: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: F_Alg E is right_complementable

let x be Element of (F_Alg E); :: thesis: x + (0. (F_Alg E)) = x
reconsider a = x as Element of E by Lm10;
thus x + (0. (F_Alg E)) = a + (0. E) by A1, Lm11
.= x ; :: thesis: verum

end;

let x be Element of (F_Alg E); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
x in Alg_El E by A2;
then consider a being F -algebraic Element of E such that
H: a = x ;
x in Alg_El E by A2;
then consider x1 being Element of E such that
A4: x = x1 ;
- a in Alg_El E ;
then reconsider y = - x1 as Element of (F_Alg E) by H, A4, d;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. (F_Alg E)
thus x + y = a + (- x1) by H, Lm11
.= 0. (F_Alg E) by A1, A4, H, RLVECT_1:5 ; :: thesis: verum