let V be RealLinearSpace; :: thesis: for M1, M2, M3 being Subset of V
for r1, r2, r3 being Real st M1 is circled & M2 is circled & M3 is circled holds
((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled
let M1, M2, M3 be Subset of V; :: thesis: for r1, r2, r3 being Real st M1 is circled & M2 is circled & M3 is circled holds
((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled
let r1, r2, r3 be Real; :: thesis: ( M1 is circled & M2 is circled & M3 is circled implies ((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled )
assume that
A1: M1 is circled and
A2: M2 is circled and
A3: M3 is circled ; :: thesis: ((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled
(r1 * M1) + (r2 * M2) is circled by A1, A2, Th3;
then (1 * ((r1 * M1) + (r2 * M2))) + (r3 * M3) is circled by A3, Th3;
hence ((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled by CONVEX1:32; :: thesis: verum