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

((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