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

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

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

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

then A --> B = {} --> B ;
hence PFuncs (A,B) = sproduct (A --> B) by Th57, PARTFUN1:48; :: 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:8;
A3: dom (A --> B) = A ;
A4: B = union (rng (A --> B)) by A2, ZFMISC_1:25;
thus PFuncs (A,B) c= sproduct (A --> B) :: thesis: sproduct (A --> B) c= PFuncs (A,B)

proof

let x be object ; :: 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 3;
A8: dom f c= dom (A --> B) by A6;

now :: thesis: for x being object st x in dom f holds
f . x in (A --> B) . x

let x be object ; :: 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 3;
then f . x in B by A7;
hence f . x in (A --> B) . x by A6, A9, FUNCOP_1:7; :: 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, Th55; :: thesis: verum

end;

end;

end;

hence PFuncs (A,B) = sproduct (A --> B) ; :: thesis: verum