let S be non empty partial quasi_total non-empty Group-like invariant TRSStr ; :: thesis: for a being Element of S st S is (R2) & S is (R9) holds

a * (a ") <<>> 1. S

let a be Element of S; :: thesis: ( S is (R2) & S is (R9) implies a * (a ") <<>> 1. S )

assume A1: ( S is (R2) & S is (R9) ) ; :: thesis: a * (a ") <<>> 1. S

take ((a ") ") * (a ") ; :: according to ABSRED_0:def 20 :: thesis: ( a * (a ") <=*= ((a ") ") * (a ") & ((a ") ") * (a ") =*=> 1. S )

(a ") " ==> a by A1;

hence ((a ") ") * (a ") =*=> a * (a ") by Th2, ThI2; :: thesis: ((a ") ") * (a ") =*=> 1. S

thus ((a ") ") * (a ") =*=> 1. S by A1, Th2; :: thesis: verum

a * (a ") <<>> 1. S

let a be Element of S; :: thesis: ( S is (R2) & S is (R9) implies a * (a ") <<>> 1. S )

assume A1: ( S is (R2) & S is (R9) ) ; :: thesis: a * (a ") <<>> 1. S

take ((a ") ") * (a ") ; :: according to ABSRED_0:def 20 :: thesis: ( a * (a ") <=*= ((a ") ") * (a ") & ((a ") ") * (a ") =*=> 1. S )

(a ") " ==> a by A1;

hence ((a ") ") * (a ") =*=> a * (a ") by Th2, ThI2; :: thesis: ((a ") ") * (a ") =*=> 1. S

thus ((a ") ") * (a ") =*=> 1. S by A1, Th2; :: thesis: verum