now

consider j being Element of J;
dom B = J by PARTFUN1:def 4;
then B . j in rng B by FUNCT_1:def 5;
then reconsider S = union (rng B) as non empty set by XBOOLE_1:3, ZFMISC_1:92;
rng p c= Funcs J,S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in Funcs J,S )
assume A1: x in rng p ; :: thesis: x in Funcs J,S
rng p c= product B by FINSEQ_1:def 4;
then consider f being Function such that
A2: ( x = f & dom f = dom B & ( for y being set st y in dom B holds
f . y in B . y ) ) by A1, CARD_3:def 5;
A3: dom B = J by PARTFUN1:def 4;
rng f c= S

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in S )
assume z in rng f ; :: thesis: z in S
then consider y being set such that
A4: ( y in dom f & z = f . y ) by FUNCT_1:def 5;
A5: z in B . y by A2, A4;
B . y in rng B by A2, A4, FUNCT_1:def 5;
then B . y c= union (rng B) by ZFMISC_1:92;
hence z in S by A5; :: thesis: verum

end;

hence x in Funcs J,S by A2, A3, FUNCT_2:def 2; :: thesis: verum

end;

then dom (uncurry p) = [:(dom p),J:] by FUNCT_5:33;
hence uncurry p is [:(dom p),J:] -defined by RELAT_1:def 18; :: thesis: verum

end;

hence uncurry p is [:(dom p),J:] -defined ; :: thesis: verum