set pf = [p,f];
reconsider C = (rng p) \/ {x} as non empty set ;
x in {x} by TARSKI:def 1;
then reconsider ox = x as Element of C by XBOOLE_0:def 3;
rng p c= C by XBOOLE_1:7;
then p is FinSequence of C by FINSEQ_1:def 4;
then reconsider pp = p as Element of C * by FINSEQ_1:def 11;
reconsider R = {[p,f]} --> ox as Function of {[p,f]},C ;
reconsider A = {[p,f]} --> pp as Function of {[p,f]},(C *) ;
reconsider S = ManySortedSign(# C,{[p,f]},A,R #) as non void strict ManySortedSign ;
take S ; :: thesis: ( the carrier of S = (rng p) \/ {x} & the carrier' of S = {[p,f]} & the Arity of S . [p,f] = p & the ResultSort of S . [p,f] = x )
[p,f] in {[p,f]} by TARSKI:def 1;
hence ( the carrier of S = (rng p) \/ {x} & the carrier' of S = {[p,f]} & the Arity of S . [p,f] = p & the ResultSort of S . [p,f] = x ) by FUNCOP_1:7; :: thesis: verum