let G1, G2 be _Graph; :: thesis: for G3 being removeLoops of G1

for G4 being removeLoops of G2

for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let G3 be removeLoops of G1; :: thesis: for G4 being removeLoops of G2

for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let G4 be removeLoops of G2; :: thesis: for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let F0 be one-to-one PGraphMapping of G1,G2; :: thesis: ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

consider F being one-to-one PGraphMapping of G3,G4 such that

A1: F = F0 | G3 and

A2: ( F0 is total implies F is total ) and

A3: ( F0 is onto implies F is onto ) and

A4: ( F0 is directed implies F is directed ) and

( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) by Th164;

take F ; :: thesis: ( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

thus F = F0 | G3 by A1; :: thesis: ( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

thus ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) by A2; :: thesis: ( ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

thus ( F0 is isomorphism implies F is isomorphism ) by A2, A3; :: thesis: ( F0 is Disomorphism implies F is Disomorphism )

thus ( F0 is Disomorphism implies F is Disomorphism ) by A2, A3, A4; :: thesis: verum

for G4 being removeLoops of G2

for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let G3 be removeLoops of G1; :: thesis: for G4 being removeLoops of G2

for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let G4 be removeLoops of G2; :: thesis: for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let F0 be one-to-one PGraphMapping of G1,G2; :: thesis: ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

consider F being one-to-one PGraphMapping of G3,G4 such that

A1: F = F0 | G3 and

A2: ( F0 is total implies F is total ) and

A3: ( F0 is onto implies F is onto ) and

A4: ( F0 is directed implies F is directed ) and

( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) by Th164;

take F ; :: thesis: ( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

thus F = F0 | G3 by A1; :: thesis: ( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

thus ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) by A2; :: thesis: ( ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

thus ( F0 is isomorphism implies F is isomorphism ) by A2, A3; :: thesis: ( F0 is Disomorphism implies F is Disomorphism )

thus ( F0 is Disomorphism implies F is Disomorphism ) by A2, A3, A4; :: thesis: verum