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;
A5: 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
thus the Source of H1 . x = the Source of G . x by A6, Def18
.= the Source of H2 . x by A2, A6, Def18 ; :: thesis: verum

end;

A7: the Source of H1 = the Source of H2 by A2, A3, A5, FUNCT_1:9;
A8: 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 A9: x in the carrier' of H1 ; :: thesis: the Target of H1 . x = the Target of H2 . x
thus the Target of H1 . x = the Target of G . x by A9, Def18
.= the Target of H2 . x by A2, A9, Def18 ; :: thesis: verum

end;

thus H1 = H2 by A1, A2, A4, A7, A8, FUNCT_1:9; :: thesis: verum