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;
A1: ( the carrier' of H c= the carrier' of G & the carrier of H c= the carrier of G ) by Def18;
A2: ( 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 A1, FUNCT_2:141, PARTFUN1:128;
A3: Funcs the carrier' of H,the carrier of H c= PFuncs the carrier' of G,the carrier of G by A2, XBOOLE_1:1;
A4: the Source of H in Funcs the carrier' of H,the carrier of H by FUNCT_2:11;
thus the Source of H in PFuncs the carrier' of G,the carrier of G by A3, A4; :: thesis: the Target of H in PFuncs the carrier' of G,the carrier of G
A5: the Target of H in Funcs the carrier' of H,the carrier of H by FUNCT_2:11;
thus the Target of H in PFuncs the carrier' of G,the carrier of G by A3, A5; :: thesis: verum