defpred S₁[ object , object ] means for h being strict Subgroup of G st h = $1 holds
$2 = the carrier of h;
A1: for e being object st e in Subgroups G holds
ex u being object st
( u in bool the carrier of G & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in Subgroups G implies ex u being object st
( u in bool the carrier of G & S₁[e,u] ) )
assume e in Subgroups G ; :: thesis: ex u being object st
( u in bool the carrier of G & S₁[e,u] )
then reconsider E = e as strict Subgroup of G by GROUP_3:def 1;
reconsider u = carr E as Subset of G ;
take u ; :: thesis: ( u in bool the carrier of G & S₁[e,u] )
thus ( u in bool the carrier of G & S₁[e,u] ) by GROUP_2:def 9; :: thesis: verum

end;

consider f being Function of (Subgroups G),(bool the carrier of G) such that
A2: for e being object st e in Subgroups G holds
S₁[e,f . e] from FUNCT_2:sch 1(A1);
take f ; :: thesis: for H being strict Subgroup of G holds f . H = the carrier of H
let H be strict Subgroup of G; :: thesis: f . H = the carrier of H
H in Subgroups G by GROUP_3:def 1;
hence f . H = the carrier of H by A2; :: thesis: verum