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

for W being Subspace of V

for x being Vector 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 Vector of (V / W) ex a being Vector of V st x = a / W

let W be Subspace of V; :: thesis: for x being Vector of (V / W) ex a being Vector of V st x = a / W

let x be Vector 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 Th15;

take a ; :: thesis: x = a / W

thus x = a / W by A1; :: thesis: verum

for W being Subspace of V

for x being Vector 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 Vector of (V / W) ex a being Vector of V st x = a / W

let W be Subspace of V; :: thesis: for x being Vector of (V / W) ex a being Vector of V st x = a / W

let x be Vector 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 Th15;

take a ; :: thesis: x = a / W

thus x = a / W by A1; :: thesis: verum