let G3, G4 be _Graph; :: thesis: for V1, V2 being set

for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let V1, V2 be set ; :: thesis: for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let G1 be addVertices of G3,V1; :: thesis: for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let G2 be addVertices of G4,V2; :: thesis: for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let F0 be PGraphMapping of G3,G4; :: thesis: for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let f be one-to-one Function; :: thesis: ( dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) implies ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) ) )

assume ( dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) ) ; :: thesis: ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

then consider F being PGraphMapping of G1,G2 such that

A1: F = [((F0 _V) +* f),(F0 _E)] and

( not F0 is empty implies not F is empty ) and

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

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

A4: ( F0 is one-to-one implies F is one-to-one ) and

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

( F0 is semi-continuous implies F is semi-continuous ) and

A6: ( F0 is continuous implies F is continuous ) and

( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) and

( F0 is Dcontinuous implies F is Dcontinuous ) by Th144;

take F ; :: thesis: ( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

thus F = [((F0 _V) +* f),(F0 _E)] by A1; :: thesis: ( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_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, A4; :: thesis: ( ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

thus ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) by A2, A4, A6; :: 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, A4; :: thesis: ( F0 is Disomorphism implies F is Disomorphism )

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

for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let V1, V2 be set ; :: thesis: for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let G1 be addVertices of G3,V1; :: thesis: for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let G2 be addVertices of G4,V2; :: thesis: for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let F0 be PGraphMapping of G3,G4; :: thesis: for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

let f be one-to-one Function; :: thesis: ( dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) implies ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) ) )

assume ( dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) ) ; :: thesis: ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

then consider F being PGraphMapping of G1,G2 such that

A1: F = [((F0 _V) +* f),(F0 _E)] and

( not F0 is empty implies not F is empty ) and

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

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

A4: ( F0 is one-to-one implies F is one-to-one ) and

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

( F0 is semi-continuous implies F is semi-continuous ) and

A6: ( F0 is continuous implies F is continuous ) and

( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) and

( F0 is Dcontinuous implies F is Dcontinuous ) by Th144;

take F ; :: thesis: ( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

thus F = [((F0 _V) +* f),(F0 _E)] by A1; :: thesis: ( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_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, A4; :: thesis: ( ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

thus ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) by A2, A4, A6; :: 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, A4; :: thesis: ( F0 is Disomorphism implies F is Disomorphism )

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