let G be Graph; :: thesis: for H being Subgraph of G holds
( the Source of H in PFuncs ( the carrier' of G, the carrier of G) & the Target of H in PFuncs ( the carrier' of G, the carrier of G) )
let H be Subgraph of G; :: thesis: ( the Source of H in PFuncs ( the carrier' of G, the carrier of G) & the Target of H in PFuncs ( the carrier' of G, the carrier of G) )
set EH = the carrier' of H;
set VH = the carrier of H;
set EG = the carrier' of G;
set VG = the carrier of G;
( the carrier' of H c= the carrier' of G & the carrier of H c= the carrier of G ) by Def18;
then ( Funcs ( the carrier' of H, the carrier of H) c= PFuncs ( the carrier' of H, the carrier of H) & PFuncs ( the carrier' of H, the carrier of H) c= PFuncs ( the carrier' of G, the carrier of G) ) by FUNCT_2:72, PARTFUN1:50;
then A1: Funcs ( the carrier' of H, the carrier of H) c= PFuncs ( the carrier' of G, the carrier of G) ;
the Source of H in Funcs ( the carrier' of H, the carrier of H) by FUNCT_2:8;
hence the Source of H in PFuncs ( the carrier' of G, the carrier of G) by A1; :: thesis: the Target of H in PFuncs ( the carrier' of G, the carrier of G)
the Target of H in Funcs ( the carrier' of H, the carrier of H) by FUNCT_2:8;
hence the Target of H in PFuncs ( the carrier' of G, the carrier of G) by A1; :: thesis: verum