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

(a ") * (a * b) <<>> b

let a, b be Element of S; :: thesis: ( S is (R1) & S is (R2) & S is (R3) implies (a ") * (a * b) <<>> b )

assume A1: ( S is (R1) & S is (R2) & S is (R3) ) ; :: thesis: (a ") * (a * b) <<>> b

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

thus ((a ") * a) * b =*=> (a ") * (a * b) by A1, Th2; :: thesis: ((a ") * a) * b =*=> b

( ((a ") * a) * b ==> (1. S) * b & (1. S) * b ==> b ) by A1, ThI2;

then ( ((a ") * a) * b =*=> (1. S) * b & (1. S) * b =*=> b ) by Th2;

hence ((a ") * a) * b =*=> b by Th3; :: thesis: verum

(a ") * (a * b) <<>> b

let a, b be Element of S; :: thesis: ( S is (R1) & S is (R2) & S is (R3) implies (a ") * (a * b) <<>> b )

assume A1: ( S is (R1) & S is (R2) & S is (R3) ) ; :: thesis: (a ") * (a * b) <<>> b

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

thus ((a ") * a) * b =*=> (a ") * (a * b) by A1, Th2; :: thesis: ((a ") * a) * b =*=> b

( ((a ") * a) * b ==> (1. S) * b & (1. S) * b ==> b ) by A1, ThI2;

then ( ((a ") * a) * b =*=> (1. S) * b & (1. S) * b =*=> b ) by Th2;

hence ((a ") * a) * b =*=> b by Th3; :: thesis: verum