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

for F2 being PGraphMapping of G2,G3 st F1 is Disomorphism & F2 is Disomorphism holds

F2 * F1 is Disomorphism

let F1 be PGraphMapping of G1,G2; :: thesis: for F2 being PGraphMapping of G2,G3 st F1 is Disomorphism & F2 is Disomorphism holds

F2 * F1 is Disomorphism

let F2 be PGraphMapping of G2,G3; :: thesis: ( F1 is Disomorphism & F2 is Disomorphism implies F2 * F1 is Disomorphism )

assume ( F1 is Disomorphism & F2 is Disomorphism ) ; :: thesis: F2 * F1 is Disomorphism

then ( F2 * F1 is directed & F2 * F1 is isomorphism ) by Th109;

hence F2 * F1 is Disomorphism ; :: thesis: verum

for F2 being PGraphMapping of G2,G3 st F1 is Disomorphism & F2 is Disomorphism holds

F2 * F1 is Disomorphism

let F1 be PGraphMapping of G1,G2; :: thesis: for F2 being PGraphMapping of G2,G3 st F1 is Disomorphism & F2 is Disomorphism holds

F2 * F1 is Disomorphism

let F2 be PGraphMapping of G2,G3; :: thesis: ( F1 is Disomorphism & F2 is Disomorphism implies F2 * F1 is Disomorphism )

assume ( F1 is Disomorphism & F2 is Disomorphism ) ; :: thesis: F2 * F1 is Disomorphism

then ( F2 * F1 is directed & F2 * F1 is isomorphism ) by Th109;

hence F2 * F1 is Disomorphism ; :: thesis: verum