let S be non empty partial quasi_total non-empty Group-like invariant TRSStr ; for a, b being Element of S st a ==> b holds
a " ==> b "
let a, b be Element of S; ( a ==> b implies a " ==> b " )
assume A0:
a ==> b
; a " ==> b "
set o = In (2,(dom the charact of S));
arity (Den ((In (2,(dom the charact of S))),S)) = 1
by ThB;
then
dom (Den ((In (2,(dom the charact of S))),S)) = 1 -tuples_on the carrier of S
by MARGREL1:22;
then reconsider aa = <*a*>, bb = <*b*> as Element of dom (Den ((In (2,(dom the charact of S))),S)) by FINSEQ_2:98;
A2:
( dom <*a*> = Seg 1 & 1 in Seg 1 )
by FINSEQ_1:1, FINSEQ_1:38;
A3:
<*a*> . 1 = a
by FINSEQ_1:40;
<*a*> +* (1,b) = <*b*>
by FUNCT_7:95;
then
(Den ((In (2,(dom the charact of S))),S)) . aa ==> (Den ((In (2,(dom the charact of S))),S)) . bb
by A0, A2, A3, DEF2;
hence
a " ==> b "
; verum