let I be set ; :: thesis: for F being ManySortedSet of I holds
( F is Group-yielding iff for i being object st i in I holds
F . i is Group )
let F be ManySortedSet of I; :: thesis: ( F is Group-yielding iff for i being object st i in I holds
F . i is Group )

hereby :: thesis: ( ( for i being object st i in I holds
F . i is Group ) implies F is Group-yielding )

assume A1: F is Group-yielding ; :: thesis: for i being object st i in I holds
F . i is Group
let i be object ; :: thesis: ( i in I implies F . i is Group )
assume i in I ; :: thesis: F . i is Group
then i in dom F by PARTFUN1:def 2;
hence F . i is Group by A1, FUNCT_1:3; :: thesis: verum

end;

assume A2: for i being object st i in I holds
F . i is Group ; :: thesis: F is Group-yielding
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 i being object such that
A3: ( i in dom F & y = F . i ) by FUNCT_1:def 3;
thus y is Group by A2, A3; :: thesis: verum

end;

hence F is Group-yielding ; :: thesis: verum