let I be set ; :: thesis:
let F be ManySortedFunction of I; :: thesis:
let Z be ManySortedSet of I; :: thesis:
assume that
A1: Z is V39() and
A2: Z c= rngs F ; :: thesis:
defpred S₁[ object , object ] means ex A being set ex f being Function st
( A = $2 & f = F . $1 & A c= (doms F) . $1 & A is finite & f .: A = Z . $1 );
A3: for i being object st i in I holds
ex j being object st S₁[i,j]

let i be object ; :: thesis:
reconsider f = F . i as Function ;
assume A4: i in I ; :: thesis:
then rng f = (rngs F) . i by Th13;
then A5: Z . i c= rng f by A2, A4;
Z . i is finite by A1;
then consider y being set such that
A6: ( y c= dom f & y is finite & f .: y = Z . i ) by A5, ORDERS_1:85;
take y ; :: thesis:
take y ; :: thesis:
take f ; :: thesis:
thus y = y ; :: thesis:
thus f = F . i ; :: thesis:
thus ( y c= (doms F) . i & y is finite & f .: y = Z . i ) by A4, A6, Th14; :: thesis:

end;

consider Y being ManySortedSet of I such that
A7: for i being object st i in I holds
S₁[i,Y . i] from PBOOLE:sch 3(A3);
take Y ; :: thesis:
thus Y c= doms F :: thesis:

let i be object ; :: according to PBOOLE:def 2 :: thesis:
assume i in I ; :: thesis:
then S₁[i,Y . i] by A7;
hence Y . i c= (doms F) . i ; :: thesis:

end;

let i be object ; :: according to FINSET_1:def 5 :: thesis:
assume i in I ; :: thesis:
then S₁[i,Y . i] by A7;
hence Y . i is finite ; :: thesis:

end;

end;