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 rng (A --> B) = {B} by FUNCOP_1:14;
then A2: ( dom (A --> B) = A & B = union (rng (A --> B)) ) by FUNCOP_1:19, 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
A3: ( x = f & dom f c= A & rng f c= B ) by PARTFUN1:def 5;
A4: dom f c= dom (A --> B) by A3, FUNCOP_1:19;

now

let x be set ; :: thesis: ( x in dom f implies f . x in (A --> B) . x )
assume A5: 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 A3;
hence f . x in (A --> B) . x by A3, A5, FUNCOP_1:13; :: thesis: verum

end;

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

end;

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

end;

end;

end;

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