set S = TotalTRS (X,x);
A3: ( the carrier of (TotalTRS (X,x)) = X & the charact of (TotalTRS (X,x)) = <*(() --> x),(() --> x),(() --> x)*> & the reduction of (TotalTRS (X,x)) = nabla X ) by DEF3;
consider f0 being non empty homogeneous quasi_total PartFunc of (X *),X such that
A0: ( arity f0 = 0 & f0 = () --> x ) by Th0;
consider f1 being non empty homogeneous quasi_total PartFunc of (X *),X such that
A1: ( arity f1 = 1 & f1 = () --> x ) by Th0;
consider f2 being non empty homogeneous quasi_total PartFunc of (X *),X such that
A2: ( arity f2 = 2 & f2 = () --> x ) by Th0;
[:X,X:] c= [:X,X:] ;
then reconsider r = [:X,X:] as Relation of X ;
reconsider a = f0, b = f1, c = f2 as Element of PFuncs ((X *),X) by PARTFUN1:45;
thus ( TotalTRS (X,x) is quasi_total & TotalTRS (X,x) is partial & TotalTRS (X,x) is Group-like ) by A0, A1, A2, A3, Th01, Th02; :: thesis: TotalTRS (X,x) is invariant
let o be OperSymbol of (TotalTRS (X,x)); :: according to ABSRED_0:def 30 :: thesis: for a, b being Element of dom (Den (o,(TotalTRS (X,x))))
for i being Nat st i in dom a holds
for x, y being Element of (TotalTRS (X,x)) st x = a . i & b = a +* (i,y) & x ==> y holds
(Den (o,(TotalTRS (X,x)))) . a ==> (Den (o,(TotalTRS (X,x)))) . b

let a, b be Element of dom (Den (o,(TotalTRS (X,x)))); :: thesis: for i being Nat st i in dom a holds
for x, y being Element of (TotalTRS (X,x)) st x = a . i & b = a +* (i,y) & x ==> y holds
(Den (o,(TotalTRS (X,x)))) . a ==> (Den (o,(TotalTRS (X,x)))) . b

let i be Nat; :: thesis: ( i in dom a implies for x, y being Element of (TotalTRS (X,x)) st x = a . i & b = a +* (i,y) & x ==> y holds
(Den (o,(TotalTRS (X,x)))) . a ==> (Den (o,(TotalTRS (X,x)))) . b )

assume i in dom a ; :: thesis: for x, y being Element of (TotalTRS (X,x)) st x = a . i & b = a +* (i,y) & x ==> y holds
(Den (o,(TotalTRS (X,x)))) . a ==> (Den (o,(TotalTRS (X,x)))) . b

let x, y be Element of (TotalTRS (X,x)); :: thesis: ( x = a . i & b = a +* (i,y) & x ==> y implies (Den (o,(TotalTRS (X,x)))) . a ==> (Den (o,(TotalTRS (X,x)))) . b )
assume ( x = a . i & b = a +* (i,y) & x ==> y ) ; :: thesis: (Den (o,(TotalTRS (X,x)))) . a ==> (Den (o,(TotalTRS (X,x)))) . b
thus [((Den (o,(TotalTRS (X,x)))) . a),((Den (o,(TotalTRS (X,x)))) . b)] in the reduction of (TotalTRS (X,x)) by ; :: according to ABSRED_0:def 1 :: thesis: verum