set P = PrimeField F;
A1: 1. (PrimeField F) = 1. F by Def10;
A2: 0. (PrimeField F) = 0. F by Def10;

hereby :: according to GROUP_1:def 3 :: thesis: ( PrimeField F is well-unital & PrimeField F is distributive & PrimeField F is almost_left_invertible )

let x, y, z be Element of (PrimeField F); :: thesis: (x * y) * z = x * (y * z)
reconsider a = x, b = y, c = z as Element of F 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;

hereby :: according to VECTSP_1:def 6 :: thesis: ( PrimeField F is distributive & PrimeField F is almost_left_invertible )

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

end;

hereby :: according to VECTSP_1:def 7 :: thesis: PrimeField F is almost_left_invertible

let x, y, z be Element of (PrimeField F); :: 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 F by Lm10;
A4: ( a * b = x * y & a * c = x * z ) by Lm12;
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)
hence (y + z) * x = (y * x) + (z * x) ; :: thesis: verum

end;

let x be Element of (PrimeField F); :: according to VECTSP_1:def 9 :: thesis: ( x = 0. (PrimeField F) or ex b₁ being Element of the carrier of (PrimeField F) st b₁ * x = 1. (PrimeField F) )
assume A5: x <> 0. (PrimeField F) ; :: thesis: ex b₁ being Element of the carrier of (PrimeField F) st b₁ * x = 1. (PrimeField F)
reconsider a = x as Element of F by Lm10;
the carrier of (PrimeField F) = carrier/\ F by Def10;
then x in carrier/\ F ;
then consider x1 being Element of F such that
A6: x = x1 and
A7: for K being Subfield of F holds x1 in K ;

now :: thesis: for K being Subfield of F holds x1 " in K

let K be Subfield of F; :: thesis: x1 " in K
x1 in K by A7;
then reconsider t = x1 as Element of K ;
t " = x1 " by A5, A6, A2, GAUSSINT:21;
hence x1 " in K ; :: thesis: verum

end;

then x1 " in carrier/\ F ;
then reconsider y = x1 " as Element of (PrimeField F) by Def10;
take y ; :: thesis: y * x = 1. (PrimeField F)
thus y * x = (x1 ") * a by Lm12
.= 1. (PrimeField F) by A1, A2, A5, A6, VECTSP_1:def 10 ; :: thesis: verum