let I be non empty set ; :: thesis: for F being Group-yielding ManySortedSet of I
for i being Element of I holds F . i is Group
let F be Group-yielding ManySortedSet of I; :: thesis: for i being Element of I holds F . i is Group
let i be Element of I; :: thesis: F . i is Group
( i in I & dom F = I ) by PARTFUN1:def 2;
then F . i in rng F by FUNCT_1:3;
hence F . i is Group by Def1; :: thesis: verum