defpred S₁[ object , object ] means for H being strict Subgroup of G1 st H = $1 holds
for A being Subset of G2 st A = f .: the carrier of H holds
$2 = gr (f .: the carrier of H);
A1: for e being object st e in the carrier of (lattice G1) holds
ex u being object st
( u in the carrier of (lattice G2) & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in the carrier of (lattice G1) implies ex u being object st
( u in the carrier of (lattice G2) & S₁[e,u] ) )
assume e in the carrier of (lattice G1) ; :: thesis: ex u being object st
( u in the carrier of (lattice G2) & S₁[e,u] )
then reconsider E = e as strict Subgroup of G1 by GROUP_3:def 1;
reconsider u = gr (f .: the carrier of E) as strict Subgroup of G2 ;
reconsider u = u as Element of (lattice G2) by GROUP_3:def 1;
take u ; :: thesis: ( u in the carrier of (lattice G2) & S₁[e,u] )
thus ( u in the carrier of (lattice G2) & S₁[e,u] ) ; :: thesis: verum

end;

consider f1 being Function of the carrier of (lattice G1), the carrier of (lattice G2) such that
A2: for e being object st e in the carrier of (lattice G1) holds
S₁[e,f1 . e] from FUNCT_2:sch 1(A1);
take f1 ; :: thesis: for H being strict Subgroup of G1
for A being Subset of G2 st A = f .: the carrier of H holds
f1 . H = gr A
let H be strict Subgroup of G1; :: thesis: for A being Subset of G2 st A = f .: the carrier of H holds
f1 . H = gr A
let A be Subset of G2; :: thesis: ( A = f .: the carrier of H implies f1 . H = gr A )
A3: H in the carrier of (lattice G1) by GROUP_3:def 1;
assume A = f .: the carrier of H ; :: thesis: f1 . H = gr A
hence f1 . H = gr A by A2, A3; :: thesis: verum