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 that
A1: the carrier of H1 = the carrier of H2 and
A2: the carrier' of H1 = the carrier' of H2 ; :: thesis: H1 = H2
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

proof

let x be object ; :: thesis: ( x in the carrier' of H1 implies the Source of H1 . x = the Source of H2 . x )
assume A5: 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 Def18
.= the Source of H2 . x by A2, A5, Def18 ;
:: thesis: verum

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

proof

let x be object ; :: thesis: ( x in the carrier' of H1 implies the Target of H1 . x = the Target of H2 . x )
assume A7: 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 Def18
.= the Target of H2 . x by A2, A7, Def18 ;
:: thesis: verum

end;

hence H1 = H2 by A1, A2, A4, A6, FUNCT_1:2; :: thesis: verum