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 (R3) & S is (R11) holds
a * (b * ((a * b) ")) <<>> 1. S
let a, b be Element of S; :: thesis: ( S is (R3) & S is (R11) implies a * (b * ((a * b) ")) <<>> 1. S )
assume A1: ( S is (R3) & S is (R11) ) ; :: thesis: a * (b * ((a * b) ")) <<>> 1. S
take (a * b) * ((a * b) ") ; :: according to ABSRED_0:def 20 :: thesis: ( a * (b * ((a * b) ")) <=*= (a * b) * ((a * b) ") & (a * b) * ((a * b) ") =*=> 1. S )
thus (a * b) * ((a * b) ") =*=> a * (b * ((a * b) ")) by A1, Th2; :: thesis: (a * b) * ((a * b) ") =*=> 1. S
thus (a * b) * ((a * b) ") =*=> 1. S by A1, Th2; :: thesis: verum