let F be Field; :: thesis: for mF being Function of [: the carrier of F,X:],X
for mo being Relation of X holds
( SymStr(# X,md,o,mF,mo #) is Abelian & SymStr(# X,md,o,mF,mo #) is add-associative & SymStr(# X,md,o,mF,mo #) is right_zeroed & SymStr(# X,md,o,mF,mo #) is right_complementable )
let mF be Function of [: the carrier of F,X:],X; :: thesis: for mo being Relation of X holds
( SymStr(# X,md,o,mF,mo #) is Abelian & SymStr(# X,md,o,mF,mo #) is add-associative & SymStr(# X,md,o,mF,mo #) is right_zeroed & SymStr(# X,md,o,mF,mo #) is right_complementable )
let mo be Relation of X; :: thesis: ( SymStr(# X,md,o,mF,mo #) is Abelian & SymStr(# X,md,o,mF,mo #) is add-associative & SymStr(# X,md,o,mF,mo #) is right_zeroed & SymStr(# X,md,o,mF,mo #) is right_complementable )
set H = SymStr(# X,md,o,mF,mo #);
A1: for x being Element of SymStr(# X,md,o,mF,mo #) holds x + (0. SymStr(# X,md,o,mF,mo #)) = x

proof

let x be Element of SymStr(# X,md,o,mF,mo #); :: thesis: x + (0. SymStr(# X,md,o,mF,mo #)) = x
md . (x,(0. SymStr(# X,md,o,mF,mo #))) = o by Lm1;
hence x + (0. SymStr(# X,md,o,mF,mo #)) = x by TARSKI:def 1; :: thesis: verum

end;

A2: SymStr(# X,md,o,mF,mo #) is right_complementable

proof

let x be Element of SymStr(# X,md,o,mF,mo #); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
take - x ; :: according to ALGSTR_0:def 11 :: thesis: x + (- x) = 0. SymStr(# X,md,o,mF,mo #)
0. SymStr(# X,md,o,mF,mo #) = o by STRUCT_0:def 6;
hence x + (- x) = 0. SymStr(# X,md,o,mF,mo #) by Lm1; :: thesis: verum

end;

A3: for x, y, z being Element of SymStr(# X,md,o,mF,mo #) holds (x + y) + z = x + (y + z)

proof

let x, y, z be Element of SymStr(# X,md,o,mF,mo #); :: thesis: (x + y) + z = x + (y + z)
reconsider x = x, y = y, z = z as Element of X ;
md . (x,(md . (y,z))) = o by Lm1;
hence (x + y) + z = x + (y + z) by Lm1; :: thesis: verum

end;

for x, y being Element of SymStr(# X,md,o,mF,mo #) holds x + y = y + x

proof

let x, y be Element of SymStr(# X,md,o,mF,mo #); :: thesis: x + y = y + x
md . (x,y) = o by Lm1;
hence x + y = y + x by Lm1; :: thesis: verum

end;

hence ( SymStr(# X,md,o,mF,mo #) is Abelian & SymStr(# X,md,o,mF,mo #) is add-associative & SymStr(# X,md,o,mF,mo #) is right_zeroed & SymStr(# X,md,o,mF,mo #) is right_complementable ) by A3, A1, A2, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum