let R be Ring; :: thesis: ( H₂(R) is Abelian & H₂(R) is add-associative & H₂(R) is right_zeroed & H₂(R) is right_complementable )
A1: for x, y, z being Scalar of
for x', y', z' being Element of st x = x' & y = y' & z = z' holds
x + y = x' + y' ;
thus H₂(R) is Abelian :: thesis: ( H₂(R) is add-associative & H₂(R) is right_zeroed & H₂(R) is right_complementable )

proof

let x, y be Element of ; :: according to RLVECT_1:def 5 :: thesis: x + y = y + x
reconsider x' = x, y' = y as Scalar of ;
thus x + y = y' + x' by A1
.= y + x ; :: thesis: verum

end;

thus H₂(R) is add-associative :: thesis: ( H₂(R) is right_zeroed & H₂(R) is right_complementable )

proof

let x, y, z be Element of ; :: according to RLVECT_1:def 6 :: thesis: (x + y) + z = x + (y + z)
reconsider x' = x, y' = y, z' = z as Scalar of ;
thus (x + y) + z = (x' + y') + z'
.= x' + (y' + z') by RLVECT_1:def 6
.= x + (y + z) ; :: thesis: verum

end;

thus H₂(R) is right_zeroed :: thesis: H₂(R) is right_complementable

proof

let x be Element of ; :: according to RLVECT_1:def 7 :: thesis: x + (0. H₂(R)) = x
reconsider x' = x as Scalar of ;
thus x + (0. H₂(R)) = x' + (0. R)
.= x by RLVECT_1:10 ; :: thesis: verum

end;

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