let K be Ring; :: thesis: for V being LeftMod of K

for A1, A2 being Subset of V st A1 <> {} & A1 c= A2 holds

for x being set st x is Vector of A1 holds

x is Vector of A2

let V be LeftMod of K; :: thesis: for A1, A2 being Subset of V st A1 <> {} & A1 c= A2 holds

for x being set st x is Vector of A1 holds

x is Vector of A2

let A1, A2 be Subset of V; :: thesis: ( A1 <> {} & A1 c= A2 implies for x being set st x is Vector of A1 holds

x is Vector of A2 )

assume that

A1: A1 <> {} and

A2: A1 c= A2 ; :: thesis: for x being set st x is Vector of A1 holds

x is Vector of A2

let x be set ; :: thesis: ( x is Vector of A1 implies x is Vector of A2 )

assume x is Vector of A1 ; :: thesis: x is Vector of A2

then reconsider a = x as Vector of A1 ;

a is Element of A1 by A1, Def11;

then a in A2 by A1, A2, TARSKI:def 3;

hence x is Vector of A2 by Def11; :: thesis: verum

for A1, A2 being Subset of V st A1 <> {} & A1 c= A2 holds

for x being set st x is Vector of A1 holds

x is Vector of A2

let V be LeftMod of K; :: thesis: for A1, A2 being Subset of V st A1 <> {} & A1 c= A2 holds

for x being set st x is Vector of A1 holds

x is Vector of A2

let A1, A2 be Subset of V; :: thesis: ( A1 <> {} & A1 c= A2 implies for x being set st x is Vector of A1 holds

x is Vector of A2 )

assume that

A1: A1 <> {} and

A2: A1 c= A2 ; :: thesis: for x being set st x is Vector of A1 holds

x is Vector of A2

let x be set ; :: thesis: ( x is Vector of A1 implies x is Vector of A2 )

assume x is Vector of A1 ; :: thesis: x is Vector of A2

then reconsider a = x as Vector of A1 ;

a is Element of A1 by A1, Def11;

then a in A2 by A1, A2, TARSKI:def 3;

hence x is Vector of A2 by Def11; :: thesis: verum