let K be Ring; :: thesis: for V being LeftMod of
for W being Subspace of V
for x being Element of V .. W ex a being Vector of st x = a .. W
let V be LeftMod of ; :: thesis: for W being Subspace of V
for x being Element of V .. W ex a being Vector of st x = a .. W
let W be Subspace of V; :: thesis: for x being Element of V .. W ex a being Vector of st x = a .. W
let x be Element of V .. W; :: thesis: ex a being Vector of st x = a .. W
consider a being Vector of such that
A1: x = a + W by Def12;
take a ; :: thesis: x = a .. W
thus x = a .. W by A1; :: thesis: verum