let S be non empty partial quasi_total non-empty Group-like invariant TRSStr ; :: thesis: for a, b, c being Element of S st a ==> b holds
a * c ==> b * c
let a, b, c be Element of S; :: thesis: ( a ==> b implies a * c ==> b * c )
assume A0: a ==> b ; :: thesis: a * c ==> b * c
set o = In (3,(dom the charact of S));
arity (Den ((In (3,(dom the charact of S))),S)) = 2 by ThB;
then dom (Den ((In (3,(dom the charact of S))),S)) = 2 -tuples_on the carrier of S by MARGREL1:22;
then reconsider ac = <*a,c*>, bc = <*b,c*> as Element of dom (Den ((In (3,(dom the charact of S))),S)) by FINSEQ_2:101;
A2: ( dom <*a,c*> = Seg 2 & 1 in Seg 2 ) by FINSEQ_1:1, FINSEQ_1:89;
A3: <*a,c*> . 1 = a by FINSEQ_1:44;
<*a,c*> +* (1,b) = <*b,c*> by COMPUT_1:1;
then (Den ((In (3,(dom the charact of S))),S)) . ac ==> (Den ((In (3,(dom the charact of S))),S)) . bc by A0, A2, A3, DEF2;
hence a * c ==> b * c ; :: thesis: verum