set P = FAdj (F,T);
A1: 1. (FAdj (F,T)) = 1. E by dFA;
A2: 0. (FAdj (F,T)) = 0. E by dFA;

now :: thesis: for x, y being Element of (FAdj (F,T)) holds x * y = y * x

let x, y be Element of (FAdj (F,T)); :: thesis: x * y = y * x
reconsider a = x, b = y as Element of E by Lm10f;
thus x * y = a * b by Lm12f
.= b * a by GROUP_1:def 12
.= y * x by Lm12f ; :: thesis: verum

end;

hence FAdj (F,T) is commutative ; :: thesis: ( FieldAdjunction (F,T) is associative & FieldAdjunction (F,T) is well-unital & FieldAdjunction (F,T) is distributive & FieldAdjunction (F,T) is almost_left_invertible )

now :: thesis: for x, y, z being Element of (FAdj (F,T)) holds (x * y) * z = x * (y * z)

let x, y, z be Element of (FAdj (F,T)); :: thesis: (x * y) * z = x * (y * z)
reconsider a = x, b = y, c = z as Element of E by Lm10f;
A3: y * z = b * c by Lm12f;
x * y = a * b by Lm12f;
hence (x * y) * z = (a * b) * c by Lm12f
.= a * (b * c) by GROUP_1:def 3
.= x * (y * z) by A3, Lm12f ;
:: thesis: verum

end;

hence FAdj (F,T) is associative ; :: thesis: ( FieldAdjunction (F,T) is well-unital & FieldAdjunction (F,T) is distributive & FieldAdjunction (F,T) is almost_left_invertible )

now :: thesis: for x being Element of (FAdj (F,T)) holds
( x * (1. (FAdj (F,T))) = x & (1. (FAdj (F,T))) * x = x )

let x be Element of (FAdj (F,T)); :: thesis: ( x * (1. (FAdj (F,T))) = x & (1. (FAdj (F,T))) * x = x )
reconsider a = x as Element of E by Lm10f;
thus x * (1. (FAdj (F,T))) = a * (1. E) by A1, Lm12f
.= x ; :: thesis: (1. (FAdj (F,T))) * x = x
thus (1. (FAdj (F,T))) * x = (1. E) * a by A1, Lm12f
.= x ; :: thesis: verum

end;

hence FAdj (F,T) is well-unital ; :: thesis: ( FieldAdjunction (F,T) is distributive & FieldAdjunction (F,T) is almost_left_invertible )

now :: thesis: for x, y, z being Element of (FAdj (F,T)) holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )

let x, y, z be Element of (FAdj (F,T)); :: 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 Lm10f;
A4: ( a * b = x * y & a * c = x * z ) by Lm12f;
A6: ( b * a = y * x & c * a = z * x ) by Lm12f;
A5: y + z = b + c by Lm11f;
hence x * (y + z) = a * (b + c) by Lm12f
.= (a * b) + (a * c) by VECTSP_1:def 7
.= (x * y) + (x * z) by A4, Lm11f ;
:: thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = (b + c) * a by A5, Lm12f
.= (b * a) + (c * a) by VECTSP_1:def 7
.= (y * x) + (z * x) by A6, Lm11f ; :: thesis: verum

end;

hence FAdj (F,T) is distributive ; :: thesis: FieldAdjunction (F,T) is almost_left_invertible

now :: thesis: for x being Element of (FAdj (F,T)) st x <> 0. (FAdj (F,T)) holds
ex y being Element of (FAdj (F,T)) st y * x = 1. (FAdj (F,T))

let x be Element of (FAdj (F,T)); :: thesis: ( x <> 0. (FAdj (F,T)) implies ex y being Element of (FAdj (F,T)) st y * x = 1. (FAdj (F,T)) )
assume A5: x <> 0. (FAdj (F,T)) ; :: thesis: ex y being Element of (FAdj (F,T)) st y * x = 1. (FAdj (F,T))
reconsider a = x as Element of E by Lm10f;
the carrier of (FAdj (F,T)) = carrierFA T by dFA;
then x in carrierFA T ;
then consider x1 being Element of E such that
A6: x = x1 and
A7: for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x1 in U ;

now :: thesis: for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x1 " in U

let U be Subfield of E; :: thesis: ( F is Subfield of U & T is Subset of U implies x1 " in U )
assume ( F is Subfield of U & T is Subset of U ) ; :: thesis: x1 " in U
then x1 in U by A7;
then reconsider t = x1 as Element of U ;
t " = x1 " by A5, A6, A2, GAUSSINT:21;
hence x1 " in U ; :: thesis: verum

end;

then x1 " in carrierFA T ;
then reconsider y = x1 " as Element of (FAdj (F,T)) by dFA;
take y = y; :: thesis: y * x = 1. (FAdj (F,T))
thus y * x = (x1 ") * a by Lm12f
.= 1. (FAdj (F,T)) by A1, A2, A5, A6, VECTSP_1:def 10 ; :: thesis: verum

end;

hence FieldAdjunction (F,T) is almost_left_invertible ; :: thesis: verum