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 Def17;
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:141, PARTFUN1:128;
then A1: Funcs the carrier' of H,the carrier of H c= PFuncs the carrier' of G,the carrier of G by XBOOLE_1:1;
the Source of H in Funcs the carrier' of H,the carrier of H by FUNCT_2:11;
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:11;
hence the Target of H in PFuncs the carrier' of G,the carrier of G by A1; :: thesis: verum