let R be Ring; :: thesis: ( H1(R) is Abelian & H1(R) is add-associative & H1(R) is right_zeroed & H1(R) is right_complementable )
A1: for x, y, z being Scalar of R
for x9, y9, z9 being Element of H1(R) st x = x9 & y = y9 & z = z9 holds
x + y = x9 + y9 ;
thus H1(R) is Abelian :: thesis: ( H1(R) is add-associative & H1(R) is right_zeroed & H1(R) is right_complementable )
proof
let x, y be Element of H1(R); :: according to RLVECT_1:def 2 :: thesis: x + y = y + x
reconsider x9 = x, y9 = y as Scalar of R ;
thus x + y = y9 + x9 by A1
.= y + x ; :: thesis: verum
end;
thus H1(R) is add-associative :: thesis: ( H1(R) is right_zeroed & H1(R) is right_complementable )
proof
let x, y, z be Element of H1(R); :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)
reconsider x9 = x, y9 = y, z9 = z as Scalar of R ;
thus (x + y) + z = (x9 + y9) + z9
.= x9 + (y9 + z9) by RLVECT_1:def 3
.= x + (y + z) ; :: thesis: verum
end;
thus H1(R) is right_zeroed :: thesis: H1(R) is right_complementable
proof
let x be Element of H1(R); :: according to RLVECT_1:def 4 :: thesis: x + (0. H1(R)) = x
reconsider x9 = x as Scalar of R ;
thus x + (0. H1(R)) = x9 + (0. R)
.= x by RLVECT_1:4 ; :: thesis: verum
end;
let x be Element of H1(R); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x9 = x as Scalar of R ;
consider b9 being Scalar of R such that
A2: x9 + b9 = 0. R by ALGSTR_0:def 11;
reconsider b = b9 as Element of H1(R) ;
take b ; :: according to ALGSTR_0:def 11 :: thesis: x + b = 0. H1(R)
thus x + b = 0. H1(R) by A2; :: thesis: verum