set S = TotalTRS (X,x);

A3: ( the carrier of (TotalTRS (X,x)) = X & the charact of (TotalTRS (X,x)) = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on 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 = (0 -tuples_on X) --> x ) by Th0;

consider f1 being non empty homogeneous quasi_total PartFunc of (X *),X such that

A1: ( arity f1 = 1 & f1 = (1 -tuples_on X) --> x ) by Th0;

consider f2 being non empty homogeneous quasi_total PartFunc of (X *),X such that

A2: ( arity f2 = 2 & f2 = (2 -tuples_on X) --> 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 A3, ZFMISC_1:87; :: according to ABSRED_0:def 1 :: thesis: verum

A3: ( the carrier of (TotalTRS (X,x)) = X & the charact of (TotalTRS (X,x)) = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on 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 = (0 -tuples_on X) --> x ) by Th0;

consider f1 being non empty homogeneous quasi_total PartFunc of (X *),X such that

A1: ( arity f1 = 1 & f1 = (1 -tuples_on X) --> x ) by Th0;

consider f2 being non empty homogeneous quasi_total PartFunc of (X *),X such that

A2: ( arity f2 = 2 & f2 = (2 -tuples_on X) --> 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 A3, ZFMISC_1:87; :: according to ABSRED_0:def 1 :: thesis: verum