let R1, R2 be Ring; :: thesis: ( H3(R1,R2) is Abelian & H3(R1,R2) is add-associative & H3(R1,R2) is right_zeroed & H3(R1,R2) is right_complementable )
set G = BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #);
A1: now :: thesis: for x, y, z being Element of BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #)) = x & ex x9 being Element of BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #) st x + x9 = 0. BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #) )
let x, y, z be Element of BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #); :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #)) = x & ex x9 being Element of BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #) st x + x9 = 0. BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #) )
A2: x + (0. BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #)) = {} by TARSKI:def 1;
( x + y = {} & (x + y) + z = {} ) by TARSKI:def 1;
hence ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #)) = x & ex x9 being Element of BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #) st x + x9 = 0. BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #) ) by A2, TARSKI:def 1; :: thesis: verum
end;
BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #) is right_complementable
proof
let x be Element of BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
take x ; :: according to ALGSTR_0:def 11 :: thesis: x + x = 0. BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #)
thus x + x = 0. BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #) by TARSKI:def 1; :: thesis: verum
end;
hence ( H3(R1,R2) is Abelian & H3(R1,R2) is add-associative & H3(R1,R2) is right_zeroed & H3(R1,R2) is right_complementable ) by A1; :: thesis: verum