set E = InducedSubfield S;
A1: ( 1. F = 1. (InducedSubfield S) & 0. F = 0. (InducedSubfield S) ) by dis;
A2: ( the carrier of (InducedSubfield S) = S & S c= the carrier of F ) by dis;

now :: thesis: for x, y being Element of (InducedSubfield S) holds x * y = y * x

let x, y be Element of (InducedSubfield S); :: thesis: x * y = y * x
reconsider a = x, b = y as Element of F by A2;
thus x * y = a * b by Lm11a
.= y * x by Lm11a ; :: thesis: verum

end;

hence InducedSubfield S is commutative ; :: thesis: ( InducedSubfield S is associative & InducedSubfield S is well-unital & InducedSubfield S is distributive & InducedSubfield S is almost_left_invertible )

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

let x, y, z be Element of (InducedSubfield S); :: thesis: (x * y) * z = x * (y * z)
reconsider a = x, b = y, c = z as Element of F by A2;
A3: y * z = b * c by Lm11a;
x * y = a * b by Lm11a;
hence (x * y) * z = (a * b) * c by Lm11a
.= a * (b * c) by GROUP_1:def 3
.= x * (y * z) by A3, Lm11a ;
:: thesis: verum

end;

hence InducedSubfield S is associative ; :: thesis: ( InducedSubfield S is well-unital & InducedSubfield S is distributive & InducedSubfield S is almost_left_invertible )

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

let x be Element of (InducedSubfield S); :: thesis: ( x * (1. (InducedSubfield S)) = x & (1. (InducedSubfield S)) * x = x )
reconsider a = x as Element of F by A2;
thus x * (1. (InducedSubfield S)) = a * (1. F) by A1, Lm11a
.= x ; :: thesis: (1. (InducedSubfield S)) * x = x
thus (1. (InducedSubfield S)) * x = (1. F) * a by A1, Lm11a
.= x ; :: thesis: verum

end;

hence InducedSubfield S is well-unital ; :: thesis: ( InducedSubfield S is distributive & InducedSubfield S is almost_left_invertible )

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

let x, y, z be Element of (InducedSubfield S); :: 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 A2;
A4: ( a * b = x * y & a * c = x * z ) by Lm11a;
A6: ( b * a = y * x & c * a = z * x ) by Lm11a;
A5: y + z = b + c by Lm11a;
hence x * (y + z) = a * (b + c) by Lm11a
.= (a * b) + (a * c) by VECTSP_1:def 7
.= (x * y) + (x * z) by A4, Lm11a ;
:: thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = (b + c) * a by A5, Lm11a
.= (b * a) + (c * a) by VECTSP_1:def 7
.= (y * x) + (z * x) by A6, Lm11a ; :: thesis: verum

end;

hence InducedSubfield S is distributive ; :: thesis: InducedSubfield S is almost_left_invertible

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

let x be Element of (InducedSubfield S); :: thesis: ( x <> 0. (InducedSubfield S) implies ex y being Element of (InducedSubfield S) st y * x = 1. (InducedSubfield S) )
assume A5: x <> 0. (InducedSubfield S) ; :: thesis: ex y being Element of (InducedSubfield S) st y * x = 1. (InducedSubfield S)
reconsider a = x as Element of F by A2;
not a is zero by dis, A5;
then reconsider y = a " as Element of (InducedSubfield S) by A2, IS;
take y = y; :: thesis: y * x = 1. (InducedSubfield S)
thus y * x = (a ") * a by Lm11a
.= 1. (InducedSubfield S) by A1, A5, VECTSP_1:def 10 ; :: thesis: verum

end;

hence InducedSubfield S is almost_left_invertible ; :: thesis: verum