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