set Fp = F |^ p;
A2: the carrier of (F |^ p) = { (a |^ p) where a is Element of F : verum } by deffp;

now :: thesis: for x being Element of (F |^ p) st x <> 0. (F |^ p) holds
ex y being Element of (F |^ p) st y * x = 1. (F |^ p)

let x be Element of (F |^ p); :: thesis: ( x <> 0. (F |^ p) implies ex y being Element of (F |^ p) st y * x = 1. (F |^ p) )
assume A5: x <> 0. (F |^ p) ; :: thesis: ex y being Element of (F |^ p) st y * x = 1. (F |^ p)
reconsider a = x as Element of F by Lm10;
x in the carrier of (F |^ p) ;
then consider b being Element of F such that
H: x = b |^ p by A2;
A6: b <> 0. F by H, A5, deffp;
(b ") |^ p in { (a |^ p) where a is Element of F : verum } ;
then reconsider y = (b ") |^ p as Element of (F |^ p) by deffp;
take y = y; :: thesis: y * x = 1. (F |^ p)
thus y * x = ((b ") |^ p) * (b |^ p) by H, Lm12
.= ((b ") * b) |^ p by BINOM:9
.= (1. F) |^ p by A6, VECTSP_1:def 10
.= 1. (F |^ p) by deffp ; :: thesis: verum

end;

hence F |^ p is almost_left_invertible by VECTSP_1:def 9; :: thesis: verum