deffunc H₁( Element of [#] (G1 .allSG())) -> inducedSubgraph of G2, rng ((F | $1) _V), rng ((F | $1) _E) = rng (F | $1);
A1: for x being Element of [#] (G1 .allSG()) holds H₁(x) in G2 .allSG() by Th1;
consider f being Function of ([#] (G1 .allSG())),(G2 .allSG()) such that
A2: for H being Element of [#] (G1 .allSG()) holds f . H = H₁(H) from GLIBPRE1:sch 1(A1);
reconsider f = f as Function of (G1 .allSG()),(G2 .allSG()) ;
take f ; :: thesis: for H being plain Subgraph of G1 holds f . H = rng (F | H)
let H be plain Subgraph of G1; :: thesis: f . H = rng (F | H)
H is Element of [#] (G1 .allSG()) by Th1;
hence f . H = rng (F | H) by A2; :: thesis: verum