consider F being ManySortedSet of F₁() such that
A1: for i being Element of F₁() holds F . i = F₂(i) from PBOOLE:sch 5();
for y being object st y in rng F holds
y is Group

proof

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

end;

then F is Group-yielding ;
then reconsider F = F as Group-Family of F₁() ;
take F ; :: thesis: for i being Element of F₁() holds F . i = F₂(i)
thus for i being Element of F₁() holds F . i = F₂(i) by A1; :: thesis: verum