now :: thesis: uncurry p is [:(dom p),J:] -defined

hence
uncurry p is [:(dom p),J:] -defined
; :: thesis: verumset j = the Element of J;

dom B = J by PARTFUN1:def 2;

then B . the Element of J in rng B by FUNCT_1:def 3;

then reconsider S = union (rng B) as non empty set by XBOOLE_1:3, ZFMISC_1:74;

rng p c= Funcs (J,S)

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

end;dom B = J by PARTFUN1:def 2;

then B . the Element of J in rng B by FUNCT_1:def 3;

then reconsider S = union (rng B) as non empty set by XBOOLE_1:3, ZFMISC_1:74;

rng p c= Funcs (J,S)

proof

then
dom (uncurry p) = [:(dom p),J:]
by FUNCT_5:26;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in Funcs (J,S) )

A1: rng p c= product B by FINSEQ_1:def 4;

assume x in rng p ; :: thesis: x in Funcs (J,S)

then consider f being Function such that

A2: x = f and

A3: dom f = dom B and

A4: for y being object st y in dom B holds

f . y in B . y by A1, CARD_3:def 5;

A5: rng f c= S

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

end;A1: rng p c= product B by FINSEQ_1:def 4;

assume x in rng p ; :: thesis: x in Funcs (J,S)

then consider f being Function such that

A2: x = f and

A3: dom f = dom B and

A4: for y being object st y in dom B holds

f . y in B . y by A1, CARD_3:def 5;

A5: rng f c= S

proof

dom B = J
by PARTFUN1:def 2;
let z be object ; :: 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 object such that

A6: y in dom f and

A7: z = f . y by FUNCT_1:def 3;

B . y in rng B by A3, A6, FUNCT_1:def 3;

then B . y c= union (rng B) by ZFMISC_1:74;

hence z in S by A3, A4, A6, A7; :: thesis: verum

end;assume z in rng f ; :: thesis: z in S

then consider y being object such that

A6: y in dom f and

A7: z = f . y by FUNCT_1:def 3;

B . y in rng B by A3, A6, FUNCT_1:def 3;

then B . y c= union (rng B) by ZFMISC_1:74;

hence z in S by A3, A4, A6, A7; :: thesis: verum

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

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