let F be Field; :: thesis: for mF being Function of [:the carrier of F,X:],X
for mo being Relation of 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 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 ; :: 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 holds x + (0. SymStr(# X,md,o,mF,mo #)) = x

proof

let x be Element of ; :: 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 ; :: 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 holds (x + y) + z = x + (y + z)

proof

let x, y, z be Element of ; :: 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 holds x + y = y + x

proof

let x, y be Element of ; :: 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 5, RLVECT_1:def 6, RLVECT_1:def 7; :: thesis: verum