let G be Graph; :: thesis:
let H1, H2 be strict Subgraph of G; :: thesis:
assume that
A1: the carrier of H1 = the carrier of H2 and
A2: the carrier' of H1 = the carrier' of H2 ; :: thesis:
A3: ( dom the Source of H1 = the carrier' of H1 & dom the Source of H2 = the carrier' of H2 ) by FUNCT_2:def 1;
A4: ( dom the Target of H1 = the carrier' of H1 & dom the Target of H2 = the carrier' of H2 ) by FUNCT_2:def 1;
for x being object st x in the carrier' of H1 holds
the Source of H1 . x = the Source of H2 . x

let x be object ; :: thesis:
assume A5: x in the carrier' of H1 ; :: thesis:
hence the Source of H1 . x = the Source of G . x by Def18
.= the Source of H2 . x by A2, A5, Def18 ;
:: thesis:

end;

then A6: the Source of H1 = the Source of H2 by A2, A3;
for x being object st x in the carrier' of H1 holds
the Target of H1 . x = the Target of H2 . x

let x be object ; :: thesis:
assume A7: x in the carrier' of H1 ; :: thesis:
hence the Target of H1 . x = the Target of G . x by Def18
.= the Target of H2 . x by A2, A7, Def18 ;
:: thesis:

end;