let S be non empty partial quasi_total non-empty Group-like invariant TRSStr ; :: thesis: for a, b being Element of S st a ==> b holds

a " ==> b "

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

assume A0: a ==> b ; :: thesis: 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 " ; :: thesis: verum

a " ==> b "

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

assume A0: a ==> b ; :: thesis: 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 " ; :: thesis: verum