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