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

proof

let x be set ; :: thesis: ( x in the carrier' of H1 implies the Source of H1 . x = the Source of H2 . x )
assume A6: x in the carrier' of H1 ; :: thesis: the Source of H1 . x = the Source of H2 . x
hence the Source of H1 . x = the Source of G . x by Def17
.= the Source of H2 . x by A1, A6, Def17 ;
:: thesis: verum

end;

then A7: the Source of H1 = the Source of H2 by A1, A2, A3, FUNCT_1:9;
for x being set st x in the carrier' of H1 holds
the Target of H1 . x = the Target of H2 . x

proof

let x be set ; :: thesis: ( x in the carrier' of H1 implies the Target of H1 . x = the Target of H2 . x )
assume A8: x in the carrier' of H1 ; :: thesis: the Target of H1 . x = the Target of H2 . x
hence the Target of H1 . x = the Target of G . x by Def17
.= the Target of H2 . x by A1, A8, Def17 ;
:: thesis: verum

end;

hence H1 = H2 by A1, A4, A5, A7, FUNCT_1:9; :: thesis: verum