let F1, F2 be Graph-yielding Function; :: thesis:
assume F1,F2 are_isomorphic ; :: thesis:
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 -isomorphic ) ;

hereby :: thesis:

assume F1 is empty ; :: thesis:
then p = {} by A1;
hence F2 is empty by A1; :: thesis:

end;

hereby :: thesis:

assume A3: F1 is loopless ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom F2 ; :: thesis:
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 -isomorphic ) by A1, A2, A4;
take G2 = G2; :: thesis:
thus F2 . x = G2 by A4, A5; :: thesis:
consider G9 being _Graph such that
A6: ( F1 . x0 = G9 & G9 is loopless ) by A1, A3, A4, GLIB_000:def 59;
thus G2 is loopless by A5, A6; :: thesis:

end;

hence F2 is loopless by GLIB_000:def 59; :: thesis:

end;

hereby :: thesis:

assume A7: F1 is non-multi ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom F2 ; :: thesis:
then consider x0 being object such that
A8: ( x0 in dom p & p . x0 = x ) by A1, FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A9: ( G1 = F1 . x0 & G2 = F2 . (p . x0) & G2 is G1 -isomorphic ) by A1, A2, A8;
take G2 = G2; :: thesis:
thus F2 . x = G2 by A8, A9; :: thesis:
consider G9 being _Graph such that
A10: ( F1 . x0 = G9 & G9 is non-multi ) by A1, A7, A8, GLIB_000:def 62;
consider G being PGraphMapping of G1,G2 such that
A11: G is isomorphism by A9, GLIB_010:def 23;
thus G2 is non-multi by A9, A10, A11, GLIB_010:89; :: thesis:

end;

hence F2 is non-multi by GLIB_000:def 62; :: thesis:

end;

hereby :: thesis:

assume A12: F1 is simple ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom F2 ; :: thesis:
then consider x0 being object such that
A13: ( x0 in dom p & p . x0 = x ) by A1, FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A14: ( G1 = F1 . x0 & G2 = F2 . (p . x0) & G2 is G1 -isomorphic ) by A1, A2, A13;
take G2 = G2; :: thesis:
thus F2 . x = G2 by A13, A14; :: thesis:
consider G9 being _Graph such that
A15: ( F1 . x0 = G9 & G9 is simple ) by A1, A12, A13, GLIB_000:def 64;
consider G being PGraphMapping of G1,G2 such that
A16: G is isomorphism by A14, GLIB_010:def 23;
thus G2 is simple by A14, A15, A16, GLIB_010:89; :: thesis:

end;

hence F2 is simple by GLIB_000:def 64; :: thesis:

end;

hereby :: thesis:

assume A17: F1 is acyclic ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom F2 ; :: thesis:
then consider x0 being object such that
A18: ( x0 in dom p & p . x0 = x ) by A1, FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A19: ( G1 = F1 . x0 & G2 = F2 . (p . x0) & G2 is G1 -isomorphic ) by A1, A2, A18;
take G2 = G2; :: thesis:
thus F2 . x = G2 by A18, A19; :: thesis:
consider G9 being _Graph such that
A20: ( F1 . x0 = G9 & G9 is acyclic ) by A1, A17, A18, GLIB_002:def 13;
consider G being PGraphMapping of G1,G2 such that
A21: G is isomorphism by A19, GLIB_010:def 23;
thus G2 is acyclic by A19, A20, A21, GLIB_010:140; :: thesis:

end;

hence F2 is acyclic by GLIB_002:def 13; :: thesis:

end;

hereby :: thesis:

assume A22: F1 is connected ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom F2 ; :: thesis:
then consider x0 being object such that
A23: ( x0 in dom p & p . x0 = x ) by A1, FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A24: ( G1 = F1 . x0 & G2 = F2 . (p . x0) & G2 is G1 -isomorphic ) by A1, A2, A23;
take G2 = G2; :: thesis:
thus F2 . x = G2 by A23, A24; :: thesis:
consider G9 being _Graph such that
A25: ( F1 . x0 = G9 & G9 is connected ) by A1, A22, A23, GLIB_002:def 12;
consider G being PGraphMapping of G1,G2 such that
A26: G is isomorphism by A24, GLIB_010:def 23;
thus G2 is connected by A24, A25, A26, GLIB_010:140; :: thesis:

end;

hence F2 is connected by GLIB_002:def 12; :: thesis:

end;

hereby :: thesis:

assume A27: F1 is Tree-like ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom F2 ; :: thesis:
then consider x0 being object such that
A28: ( x0 in dom p & p . x0 = x ) by A1, FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A29: ( G1 = F1 . x0 & G2 = F2 . (p . x0) & G2 is G1 -isomorphic ) by A1, A2, A28;
take G2 = G2; :: thesis:
thus F2 . x = G2 by A28, A29; :: thesis:
consider G9 being _Graph such that
A30: ( F1 . x0 = G9 & G9 is Tree-like ) by A1, A27, A28, GLIB_002:def 14;
consider G being PGraphMapping of G1,G2 such that
A31: G is isomorphism by A29, GLIB_010:def 23;
( G2 is connected & G2 is acyclic ) by A29, A30, A31, GLIB_010:140;
hence G2 is Tree-like ; :: thesis:

end;

hence F2 is Tree-like by GLIB_002:def 14; :: thesis:

end;

hereby :: thesis:

assume A32: F1 is chordal ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom F2 ; :: thesis:
then consider x0 being object such that
A33: ( x0 in dom p & p . x0 = x ) by A1, FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A34: ( G1 = F1 . x0 & G2 = F2 . (p . x0) & G2 is G1 -isomorphic ) by A1, A2, A33;
take G2 = G2; :: thesis:
thus F2 . x = G2 by A33, A34; :: thesis:
consider G9 being _Graph such that
A35: ( F1 . x0 = G9 & G9 is chordal ) by A1, A32, A33, GLIBPRE0:def 4;
consider G being PGraphMapping of G1,G2 such that
A36: G is isomorphism by A34, GLIB_010:def 23;
thus G2 is chordal by A34, A35, A36, GLIB_010:140; :: thesis:

end;

hence F2 is chordal by GLIBPRE0:def 4; :: thesis:

end;

hereby :: thesis:

assume A37: F1 is edgeless ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom F2 ; :: thesis:
then consider x0 being object such that
A38: ( x0 in dom p & p . x0 = x ) by A1, FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A39: ( G1 = F1 . x0 & G2 = F2 . (p . x0) & G2 is G1 -isomorphic ) by A1, A2, A38;
take G2 = G2; :: thesis:
thus F2 . x = G2 by A38, A39; :: thesis:
consider G9 being _Graph such that
A40: ( F1 . x0 = G9 & G9 is edgeless ) by A1, A37, A38, GLIB_008:def 2;
consider G being PGraphMapping of G1,G2 such that
A41: G is isomorphism by A39, GLIB_010:def 23;
thus G2 is edgeless by A39, A40, A41, GLIB_010:89; :: thesis:

end;

hence F2 is edgeless by GLIB_008:def 2; :: thesis:

end;

hereby :: thesis:

assume A42: F1 is loopfull ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom F2 ; :: thesis:
then consider x0 being object such that
A43: ( x0 in dom p & p . x0 = x ) by A1, FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A44: ( G1 = F1 . x0 & G2 = F2 . (p . x0) & G2 is G1 -isomorphic ) by A1, A2, A43;
take G2 = G2; :: thesis:
thus F2 . x = G2 by A43, A44; :: thesis:
consider G9 being _Graph such that
A45: ( F1 . x0 = G9 & G9 is loopfull ) by A1, A42, A43, GLIB_012:def 2;
consider G being PGraphMapping of G1,G2 such that
A46: G is isomorphism by A44, GLIB_010:def 23;
thus G2 is loopfull by A44, A45, A46, GLIB_012:10; :: thesis:

end;

hence F2 is loopfull by GLIB_012:def 2; :: thesis:

end;