set P = F_Alg E;
A1: 1. (F_Alg E) = 1. E by d;
A2: 0. (F_Alg E) = 0. E by d;

now :: thesis: for x, y being Element of (F_Alg E) holds x * y = y * x

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 Lm12
.= b * a by GROUP_1:def 12
.= y * x by Lm12 ; :: thesis: verum

end;

hence F_Alg E is commutative ; :: thesis: ( F_Alg E is associative & F_Alg E is well-unital & F_Alg E is distributive & F_Alg E is almost_left_invertible )

now :: thesis: for x, y, z being Element of (F_Alg E) holds (x * y) * z = x * (y * z)

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 Lm12;
x * y = a * b by Lm12;
hence (x * y) * z = (a * b) * c by Lm12
.= a * (b * c) by GROUP_1:def 3
.= x * (y * z) by A3, Lm12 ;
:: thesis: verum

end;

hence F_Alg E is associative ; :: thesis: ( F_Alg E is well-unital & F_Alg E is distributive & F_Alg E is almost_left_invertible )

now :: thesis: for x being Element of (F_Alg E) holds
( x * (1. (F_Alg E)) = x & (1. (F_Alg E)) * x = x )

let x be Element of (F_Alg E); :: thesis: ( x * (1. (F_Alg E)) = x & (1. (F_Alg E)) * x = x )
reconsider a = x as Element of E by Lm10;
thus x * (1. (F_Alg E)) = a * (1. E) by A1, Lm12
.= x ; :: thesis: (1. (F_Alg E)) * x = x
thus (1. (F_Alg E)) * x = (1. E) * a by A1, Lm12
.= x ; :: thesis: verum

end;

hence F_Alg E is well-unital ; :: thesis: ( F_Alg E is distributive & F_Alg E is almost_left_invertible )

now :: thesis: for x, y, z being Element of (F_Alg E) holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )

let x, y, z be Element of (F_Alg E); :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider a = x, b = y, c = z as Element of E by Lm10;
A4: ( a * b = x * y & a * c = x * z ) by Lm12;
A6: ( b * a = y * x & c * a = z * x ) by Lm12;
A5: y + z = b + c by Lm11;
hence x * (y + z) = a * (b + c) by Lm12
.= (a * b) + (a * c) by VECTSP_1:def 7
.= (x * y) + (x * z) by A4, Lm11 ;
:: thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = (b + c) * a by A5, Lm12
.= (b * a) + (c * a) by VECTSP_1:def 7
.= (y * x) + (z * x) by A6, Lm11 ; :: thesis: verum

end;

hence F_Alg E is distributive ; :: thesis: F_Alg E is almost_left_invertible

now :: thesis: for x being Element of (F_Alg E) st x <> 0. (F_Alg E) holds
ex y being Element of (F_Alg E) st y * x = 1. (F_Alg E)

let x be Element of (F_Alg E); :: thesis: ( x <> 0. (F_Alg E) implies ex y being Element of (F_Alg E) st y * x = 1. (F_Alg E) )
assume A5: x <> 0. (F_Alg E) ; :: thesis: ex y being Element of (F_Alg E) st y * x = 1. (F_Alg E)
reconsider a = x as Element of E by Lm10;
the carrier of (F_Alg E) = Alg_El E by d;
then x in Alg_El E ;
then consider x1 being F -algebraic Element of E such that
A6: x = x1 ;
not x1 is zero by d, A5, A6;
then x1 " in Alg_El E ;
then reconsider y = x1 " as Element of (F_Alg E) by d;
take y = y; :: thesis: y * x = 1. (F_Alg E)
thus y * x = (x1 ") * a by Lm12
.= 1. (F_Alg E) by A1, A2, A5, A6, VECTSP_1:def 10 ; :: thesis: verum

end;

hence F_Alg E is almost_left_invertible ; :: thesis: verum