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

proof

let x, y be Element of SymStr(# {0},md,o,mF,mo #); :: according to RLVECT_1:def 2 :: thesis: x + y = y + x
reconsider x = x, y = y as Element of {0} ;
md . (x,y) = o by Lm1;
hence x + y = y + x by Lm1; :: thesis: verum

end;

thus SymStr(# {0},md,o,mF,mo #) is add-associative :: thesis: ( SymStr(# {0},md,o,mF,mo #) is right_zeroed & SymStr(# {0},md,o,mF,mo #) is right_complementable )

proof

let x, y, z be Element of SymStr(# {0},md,o,mF,mo #); :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)
reconsider x = x, y = y, z = z as Element of {0} ;
md . (x,(md . (y,z))) = o by Lm1;
hence (x + y) + z = x + (y + z) by Lm1; :: thesis: verum

end;

thus SymStr(# {0},md,o,mF,mo #) is right_zeroed :: thesis: SymStr(# {0},md,o,mF,mo #) is right_complementable

proof

let x be Element of SymStr(# {0},md,o,mF,mo #); :: according to RLVECT_1:def 4 :: thesis: x + (0. SymStr(# {0},md,o,mF,mo #)) = x
reconsider x = x as Element of {0} ;
md . (x,(0. SymStr(# {0},md,o,mF,mo #))) = o by Lm1;
hence x + (0. SymStr(# {0},md,o,mF,mo #)) = x by TARSKI:def 1; :: thesis: verum

end;

let x be Element of SymStr(# {0},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(# {0},md,o,mF,mo #)
thus x + (- x) = 0. SymStr(# {0},md,o,mF,mo #) by Lm1; :: thesis: verum