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

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

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

assume ( S is (R8) & S is (R9) ) ; :: thesis: ((a ") ") * (1. S) =*=> a

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

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

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

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

assume ( S is (R8) & S is (R9) ) ; :: thesis: ((a ") ") * (1. S) =*=> a

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

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