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:
let o be OperSymbol of (TotalTRS (X,x)); :: according to ABSRED_0:def 30 :: thesis:
let a, b be Element of dom (Den (o,(TotalTRS (X,x)))); :: thesis:
let i be Nat; :: thesis:
assume i in dom a ; :: thesis:
let x, y be Element of (TotalTRS (X,x)); :: thesis:
assume ( x = a . i & b = a +* (i,y) & x ==> y ) ; :: thesis:
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: