let I be set ; :: thesis: for A being ManySortedSet of I
for F being ManySortedFunction of I st A c= rngs F & ( for i being set
for f being Function st i in I & f = F . i holds
f " (A . i) is finite ) holds
A is finite-yielding
let A be ManySortedSet of I; :: thesis: for F being ManySortedFunction of I st A c= rngs F & ( for i being set
for f being Function st i in I & f = F . i holds
f " (A . i) is finite ) holds
A is finite-yielding
let F be ManySortedFunction of I; :: thesis: ( A c= rngs F & ( for i being set
for f being Function st i in I & f = F . i holds
f " (A . i) is finite ) implies A is finite-yielding )
assume that
A1: A c= rngs F and
A2: for i being set
for f being Function st i in I & f = F . i holds
f " (A . i) is finite ; :: thesis: A is finite-yielding
let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or A . i is finite )
assume A3: i in I ; :: thesis: A . i is finite
reconsider f = F . i as Function ;
(rngs F) . i = rng f by A3, Th13;
then A4: A . i c= rng f by A1, A3;
f " (A . i) is finite by A2, A3;
hence A . i is finite by A4, FINSET_1:9; :: thesis: verum