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