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

((a ") ") * b =*=> a * b

let a, b be Element of S; :: thesis: ( S is (R9) implies ((a ") ") * b =*=> a * b )

assume S is (R9) ; :: thesis: ((a ") ") * b =*=> a * b

then (a ") " ==> a ;

hence ((a ") ") * b =*=> a * b by Th2, ThI2; :: thesis: verum

((a ") ") * b =*=> a * b

let a, b be Element of S; :: thesis: ( S is (R9) implies ((a ") ") * b =*=> a * b )

assume S is (R9) ; :: thesis: ((a ") ") * b =*=> a * b

then (a ") " ==> a ;

hence ((a ") ") * b =*=> a * b by Th2, ThI2; :: thesis: verum