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 (R11) & S is (R14) holds

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

let a, b be Element of S; :: thesis: ( S is (R11) & S is (R14) implies a * (b * ((a * b) ")) =*=> 1. S )

assume A1: ( S is (R11) & S is (R14) ) ; :: thesis: a * (b * ((a * b) ")) =*=> 1. S

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

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

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

let a, b be Element of S; :: thesis: ( S is (R11) & S is (R14) implies a * (b * ((a * b) ")) =*=> 1. S )

assume A1: ( S is (R11) & S is (R14) ) ; :: thesis: a * (b * ((a * b) ")) =*=> 1. S

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

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