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

c * a ==> c * b

let a, b, c be Element of S; :: thesis: ( a ==> b implies c * a ==> c * b )

assume A0: a ==> b ; :: thesis: c * a ==> c * b

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 = <*c,a*>, bc = <*c,b*> as Element of dom (Den ((In (3,(dom the charact of S))),S)) by FINSEQ_2:101;

A2: ( dom <*c,a*> = Seg 2 & 2 in Seg 2 ) by FINSEQ_1:1, FINSEQ_1:89;

A3: <*c,a*> . 2 = a by FINSEQ_1:44;

<*c,a*> +* (2,b) = <*c,b*> 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 c * a ==> c * b ; :: thesis: verum

c * a ==> c * b

let a, b, c be Element of S; :: thesis: ( a ==> b implies c * a ==> c * b )

assume A0: a ==> b ; :: thesis: c * a ==> c * b

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 = <*c,a*>, bc = <*c,b*> as Element of dom (Den ((In (3,(dom the charact of S))),S)) by FINSEQ_2:101;

A2: ( dom <*c,a*> = Seg 2 & 2 in Seg 2 ) by FINSEQ_1:1, FINSEQ_1:89;

A3: <*c,a*> . 2 = a by FINSEQ_1:44;

<*c,a*> +* (2,b) = <*c,b*> 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 c * a ==> c * b ; :: thesis: verum