let K be Ring; :: thesis: for V being LeftMod of K
for W being Subspace of V holds
( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )
let V be LeftMod of K; :: thesis: for W being Subspace of V holds
( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )
let W be Subspace of V; :: thesis: ( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )
A1: for x, y, z being Element of (V . W)
for x', y', z' being Vector of (V / W) st x = x' & y = y' & z = z' holds
x + y = x' + y' ;
thus V / W is Abelian :: thesis: ( V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )

proof

let x, y be Vector of (V / W); :: according to RLVECT_1:def 5 :: thesis: x + y = y + x
reconsider x' = x, y' = y as Element of (V . W) ;
thus x + y = x' + y'
.= y + x by A1 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 6 :: thesis: ( V / W is right_zeroed & V / W is right_complementable )

let x, y, z be Vector of (V / W); :: thesis: (x + y) + z = x + (y + z)
reconsider x' = x, y' = y, z' = z as Element of (V . W) ;
thus (x + y) + z = (x' + y') + z'
.= x' + (y' + z') by RLVECT_1:def 6
.= x + (y + z) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 7 :: thesis: V / W is right_complementable

let x be Vector of (V / W); :: thesis: x + (0. (V / W)) = x
reconsider x' = x as Element of (V . W) ;
thus x + (0. (V / W)) = x' + (0. (V . W))
.= x by RLVECT_1:10 ; :: thesis: verum

end;

let x be Vector of (V / W); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x' = x as Element of (V . W) ;
consider b being Element of (V . W) such that
A2: x' + b = 0. (V . W) by ALGSTR_0:def 11;
reconsider b' = b as Vector of (V / W) ;
take b' ; :: according to ALGSTR_0:def 11 :: thesis: x + b' = 0. (V / W)
thus x + b' = 0. (V / W) by A2; :: thesis: verum