let F1, F2 be Graph-yielding Function; :: thesis: ( F1,F2 are_Disomorphic implies ( ( F1 is non-Dmulti implies F2 is non-Dmulti ) & ( F1 is Dsimple implies F2 is Dsimple ) ) )
assume F1,F2 are_Disomorphic ; :: thesis: ( ( F1 is non-Dmulti implies F2 is non-Dmulti ) & ( F1 is Dsimple implies F2 is Dsimple ) )
then consider p being one-to-one Function such that
A1: ( dom p = dom F1 & rng p = dom F2 ) and
A2: for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) ;
hereby :: thesis: ( F1 is Dsimple implies F2 is Dsimple )
assume A3: F1 is non-Dmulti ; :: thesis: F2 is non-Dmulti
now :: thesis: for x being object st x in dom F2 holds
ex G2 being _Graph st
( F2 . x = G2 & G2 is non-Dmulti )
let x be object ; :: thesis: ( x in dom F2 implies ex G2 being _Graph st
( F2 . x = G2 & G2 is non-Dmulti ) )
assume x in dom F2 ; :: thesis: ex G2 being _Graph st
( F2 . x = G2 & G2 is non-Dmulti )
then consider x0 being object such that
A4: ( x0 in dom p & p . x0 = x ) by A1, FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A5: ( G1 = F1 . x0 & G2 = F2 . (p . x0) & G2 is G1 -Disomorphic ) by A1, A2, A4;
take G2 = G2; :: thesis: ( F2 . x = G2 & G2 is non-Dmulti )
thus F2 . x = G2 by A4, A5; :: thesis: G2 is non-Dmulti
consider G9 being _Graph such that
A6: ( F1 . x0 = G9 & G9 is non-Dmulti ) by A1, A3, A4, GLIB_000:def 63;
consider G being PGraphMapping of G1,G2 such that
A7: G is Disomorphism by A5, GLIB_010:def 24;
thus G2 is non-Dmulti by A5, A6, A7, GLIB_010:90; :: thesis: verum
end;
hence F2 is non-Dmulti by GLIB_000:def 63; :: thesis: verum
end;
hereby :: thesis: verum
assume A8: F1 is Dsimple ; :: thesis: F2 is Dsimple
now :: thesis: for x being object st x in dom F2 holds
ex G2 being _Graph st
( F2 . x = G2 & G2 is Dsimple )
let x be object ; :: thesis: ( x in dom F2 implies ex G2 being _Graph st
( F2 . x = G2 & G2 is Dsimple ) )
assume x in dom F2 ; :: thesis: ex G2 being _Graph st
( F2 . x = G2 & G2 is Dsimple )
then consider x0 being object such that
A9: ( x0 in dom p & p . x0 = x ) by A1, FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A10: ( G1 = F1 . x0 & G2 = F2 . (p . x0) & G2 is G1 -Disomorphic ) by A1, A2, A9;
take G2 = G2; :: thesis: ( F2 . x = G2 & G2 is Dsimple )
thus F2 . x = G2 by A9, A10; :: thesis: G2 is Dsimple
consider G9 being _Graph such that
A11: ( F1 . x0 = G9 & G9 is Dsimple ) by A1, A8, A9, GLIB_000:def 65;
consider G being PGraphMapping of G1,G2 such that
A12: G is Disomorphism by A10, GLIB_010:def 24;
thus G2 is Dsimple by A10, A11, A12, GLIB_010:90; :: thesis: verum
end;
hence F2 is Dsimple by GLIB_000:def 65; :: thesis: verum
end;