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