now :: thesis: for x, y being VECTOR of V

for r being Real st 0 < r & r < 1 & x in M /\ N & y in M /\ N holds

(r * x) + ((1 - r) * y) in M /\ N

hence
for bfor r being Real st 0 < r & r < 1 & x in M /\ N & y in M /\ N holds

(r * x) + ((1 - r) * y) in M /\ N

let x, y be VECTOR of V; :: thesis: for r being Real st 0 < r & r < 1 & x in M /\ N & y in M /\ N holds

(r * x) + ((1 - r) * y) in M /\ N

let r be Real; :: thesis: ( 0 < r & r < 1 & x in M /\ N & y in M /\ N implies (r * x) + ((1 - r) * y) in M /\ N )

assume that

A1: ( 0 < r & r < 1 ) and

A2: ( x in M /\ N & y in M /\ N ) ; :: thesis: (r * x) + ((1 - r) * y) in M /\ N

( x in N & y in N ) by A2, XBOOLE_0:def 4;

then A3: (r * x) + ((1 - r) * y) in N by A1, Def2;

( x in M & y in M ) by A2, XBOOLE_0:def 4;

then (r * x) + ((1 - r) * y) in M by A1, Def2;

hence (r * x) + ((1 - r) * y) in M /\ N by A3, XBOOLE_0:def 4; :: thesis: verum

end;(r * x) + ((1 - r) * y) in M /\ N

let r be Real; :: thesis: ( 0 < r & r < 1 & x in M /\ N & y in M /\ N implies (r * x) + ((1 - r) * y) in M /\ N )

assume that

A1: ( 0 < r & r < 1 ) and

A2: ( x in M /\ N & y in M /\ N ) ; :: thesis: (r * x) + ((1 - r) * y) in M /\ N

( x in N & y in N ) by A2, XBOOLE_0:def 4;

then A3: (r * x) + ((1 - r) * y) in N by A1, Def2;

( x in M & y in M ) by A2, XBOOLE_0:def 4;

then (r * x) + ((1 - r) * y) in M by A1, Def2;

hence (r * x) + ((1 - r) * y) in M /\ N by A3, XBOOLE_0:def 4; :: thesis: verum

b