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

proof

let i be set ; :: thesis: ( i in I implies ex j being set st S₁[i,j] )
reconsider f = F . i as Function ;
assume A4: i in I ; :: thesis: ex j being set st S₁[i,j]
then rng f = (rngs F) . i by Th13;
then A5: Z . i c= rng f by A2, A4, PBOOLE:def 2;
Z . i is finite by A1, A4, Lm1;
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: S₁[i,y]
take f ; :: thesis: ( f = F . i & y c= (doms F) . i & y is finite & f .: y = Z . i )
thus f = F . i ; :: thesis: ( y c= (doms F) . i & y is finite & f .: y = Z . i )
thus ( y c= (doms F) . i & y is finite & f .: y = Z . i ) by A4, A6, Th14; :: thesis: verum

end;

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

proof

let i be set ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or Y . i c= (doms F) . i )
assume i in I ; :: thesis: Y . i c= (doms F) . i
then ex f being Function st
( f = F . i & Y . i c= (doms F) . i & Y . i is finite & f .: (Y . i) = Z . i ) by A7;
hence Y . i c= (doms F) . i ; :: thesis: verum

end;

thus Y is finite-yielding :: thesis: F .:.: Y = Z

proof

let i be set ; :: according to FINSET_1:def 4 :: thesis: ( not i in I or Y . i is finite )
assume i in I ; :: thesis: Y . i is finite
then ex f being Function st
( f = F . i & Y . i c= (doms F) . i & Y . i is finite & f .: (Y . i) = Z . i ) by A7;
hence Y . i is finite ; :: thesis: verum

end;

now

let i be set ; :: thesis: ( i in I implies (F .:.: Y) . i = Z . i )
assume A8: i in I ; :: thesis: (F .:.: Y) . i = Z . i
then ex f being Function st
( f = F . i & Y . i c= (doms F) . i & Y . i is finite & f .: (Y . i) = Z . i ) by A7;
hence (F .:.: Y) . i = Z . i by A8, PBOOLE:def 20; :: thesis: verum

end;

hence F .:.: Y = Z by PBOOLE:3; :: thesis: verum