let x be set ; :: thesis: for K being Ring
for M, N being LeftMod of K st M c= N holds
( ( x in M implies x in N ) & ( x is Vector of M implies x is Vector of N ) )
let K be Ring; :: thesis: for M, N being LeftMod of K st M c= N holds
( ( x in M implies x in N ) & ( x is Vector of M implies x is Vector of N ) )
let M, N be LeftMod of K; :: thesis: ( M c= N implies ( ( x in M implies x in N ) & ( x is Vector of M implies x is Vector of N ) ) )
assume A1: M c= N ; :: thesis: ( ( x in M implies x in N ) & ( x is Vector of M implies x is Vector of N ) )
thus ( x in M implies x in N ) :: thesis: ( x is Vector of M implies x is Vector of N )

proof

reconsider M9 = M as Subspace of N by A1, Def7;
assume x in M ; :: thesis: x in N
then x in M9 ;
hence x in N by VECTSP_4:9; :: thesis: verum

end;

thus ( x is Vector of M implies x is Vector of N ) :: thesis: verum

proof

reconsider M9 = M as Subspace of N by A1, Def7;
assume x is Vector of M ; :: thesis: x is Vector of N
then x is Vector of M9 ;
hence x is Vector of N by VECTSP_4:10; :: thesis: verum

end;