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 (R4) holds

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

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

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

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

(a ") * a ==> 1. S by A1;

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

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

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

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

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

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

(a ") * a ==> 1. S by A1;

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

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