let A, B be set ; :: thesis: PFuncs A,B = sproduct (A --> B)

now

per cases ( A = {} or A <> {} ) ;

case A1: A = {} ; :: thesis: PFuncs A,B = sproduct (A --> B)

then A --> B = {} --> B ;
hence PFuncs A,B = sproduct (A --> B) by A1, Th73, PARTFUN1:122; :: thesis: verum

end;

case A <> {} ; :: thesis: ( PFuncs A,B c= sproduct (A --> B) & sproduct (A --> B) c= PFuncs A,B )

then A2: rng (A --> B) = {B} by FUNCOP_1:14;
A3: dom (A --> B) = A by FUNCOP_1:19;
A4: B = union (rng (A --> B)) by A2, ZFMISC_1:31;
thus PFuncs A,B c= sproduct (A --> B) :: thesis: sproduct (A --> B) c= PFuncs A,B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in PFuncs A,B or x in sproduct (A --> B) )
assume x in PFuncs A,B ; :: thesis: x in sproduct (A --> B)
then consider f being Function such that
A5: x = f and
A6: dom f c= A and
A7: rng f c= B by PARTFUN1:def 5;
A8: dom f c= dom (A --> B) by A6, FUNCOP_1:19;

now

let x be set ; :: thesis: ( x in dom f implies f . x in (A --> B) . x )
assume A9: x in dom f ; :: thesis: f . x in (A --> B) . x
then f . x in rng f by FUNCT_1:def 5;
then f . x in B by A7;
hence f . x in (A --> B) . x by A6, A9, FUNCOP_1:13; :: thesis: verum

end;

hence x in sproduct (A --> B) by A5, A8, Def9; :: thesis: verum

end;

thus sproduct (A --> B) c= PFuncs A,B by A3, A4, Th71; :: thesis: verum

end;

end;

end;

hence PFuncs A,B = sproduct (A --> B) by XBOOLE_0:def 10; :: thesis: verum