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;
set r = nabla X;
reconsider a = f0, b = f1, c = f2 as Element of PFuncs ((X *),X) by PARTFUN1:45;
reconsider O = <*a,b,c*> as non-empty non empty PFuncFinSequence of X ;
take S = TRSStr(# X,O,(nabla X) #); :: thesis: ( the carrier of S = X & the charact of S = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on X) --> x)*> & the reduction of S = nabla X )
thus ( the carrier of S = X & the charact of S = <*((0 -tuples_on X) --> x),((1 -tuples_on X) --> x),((2 -tuples_on X) --> x)*> & the reduction of S = nabla X ) by A0, A1, A2; :: thesis: verum