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
; ( 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; verum