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

hereby :: according to RLVECT_1:def 2 :: thesis: ( InducedSubfield S is add-associative & InducedSubfield S is right_zeroed & InducedSubfield S is right_complementable )

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;

hereby :: according to RLVECT_1:def 3 :: thesis: ( InducedSubfield S is right_zeroed & InducedSubfield S is right_complementable )

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 RLVECT_1:def 3
.= x + (y + z) by A3, Lm11a ;
:: thesis: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: InducedSubfield S is right_complementable

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

end;

now :: thesis: for x being Element of (InducedSubfield S) holds x is right_complementable

let x be Element of (InducedSubfield S); :: thesis: x is right_complementable
reconsider a = x as Element of F by A2;
reconsider y = - a as Element of (InducedSubfield S) by A2, IS;
x + y = a + (- a) by Lm11a
.= 0. F by RLVECT_1:5
.= 0. (InducedSubfield S) by dis ;
hence x is right_complementable ; :: thesis: verum

end;

hence InducedSubfield S is right_complementable ; :: thesis: verum