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 5 :: thesis: x + y = y + x
reconsider x = x, y = y as Element of {0 } ;
( md . x,y = o & md . y,x = o ) by Lm1;
hence x + y = y + x ; :: 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 6 :: 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 7 :: 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