let I be set ; :: thesis: for B, A being ManySortedSet of I st B is non-empty & [|A,B|] is locally-finite holds
A is locally-finite
let B, A be ManySortedSet of I; :: thesis: ( B is non-empty & [|A,B|] is locally-finite implies A is locally-finite )
assume A1: ( B is non-empty & [|A,B|] is locally-finite ) ; :: thesis: A is locally-finite
let i be set ; :: according to PRE_CIRC:def 3 :: thesis: ( not i in I or A . i is finite )
assume A2: i in I ; :: thesis: A . i is finite
then [|A,B|] . i is finite by A1, PRE_CIRC:def 3;
then ( B . i <> {} & [:(A . i),(B . i):] is finite ) by A1, A2, PBOOLE:def 21;
hence A . i is finite ; :: thesis: verum