defpred S₁[ Element of F₁(), object ] means ex j being Subgroup of F₂() . $1 st
( $2 = j & P₁[$1,j] );
A2: for i being Element of F₁() ex j being object st S₁[i,j]

proof

let i be Element of F₁(); :: thesis: ex j being object st S₁[i,j]
consider j being Subgroup of F₂() . i such that
B1: P₁[i,j] by A1;
take j ; :: thesis: S₁[i,j]
thus S₁[i,j] by B1; :: thesis: verum

end;

consider S being ManySortedSet of F₁() such that
A3: for i being Element of F₁() holds S₁[i,S . i] from PBOOLE:sch 6(A2);
for y being object st y in rng S holds
y is Group

proof

let y be object ; :: thesis: ( y in rng S implies y is Group )
assume y in rng S ; :: thesis: y is Group
then consider x being object such that
B2: ( x in dom S & y = S . x ) by FUNCT_1:def 3;
reconsider i = x as Element of F₁() by B2;
S₁[i,y] by A3, B2;
hence y is Group ; :: thesis: verum

end;

then S is Group-yielding ;
then reconsider S = S as Group-Family of F₁() ;
for i being Element of F₁() holds S . i is Subgroup of F₂() . i

proof

let i be Element of F₁(); :: thesis: S . i is Subgroup of F₂() . i
S₁[i,S . i] by A3;
hence S . i is Subgroup of F₂() . i ; :: thesis: verum

end;

then S is F₂() -Subgroup-yielding ;
then reconsider S = S as Subgroup-Family of F₂() ;
take S ; :: thesis: for i being Element of F₁() holds P₁[i,S . i]
thus for i being Element of F₁() holds P₁[i,S . i] :: thesis: verum

proof

let i be Element of F₁(); :: thesis: P₁[i,S . i]
S₁[i,S . i] by A3;
hence P₁[i,S . i] ; :: thesis: verum

end;