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

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

let a be Element of S; :: thesis: ( S is (R1) & S is (R10) implies ((1. S) ") * a =*=> a )

assume A1: ( S is (R1) & S is (R10) ) ; :: thesis: ((1. S) ") * a =*=> a

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

hence ((1. S) ") * a =*=> a by Lem3; :: thesis: verum

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

let a be Element of S; :: thesis: ( S is (R1) & S is (R10) implies ((1. S) ") * a =*=> a )

assume A1: ( S is (R1) & S is (R10) ) ; :: thesis: ((1. S) ") * a =*=> a

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

hence ((1. S) ") * a =*=> a by Lem3; :: thesis: verum