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₁[ 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]

proof

let i be object ; :: thesis: ( i in I implies ex j being object st S₁[i,j] )
reconsider f = F . i as Function ;
assume A4: i in I ; :: thesis: ex j being object st S₁[i,j]
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: S₁[i,y]
take y ; :: thesis: ex f being Function st
( y = y & f = F . i & y c= (doms F) . i & y is finite & f .: y = Z . i )
take f ; :: thesis: ( y = y & f = F . i & y c= (doms F) . i & y is finite & f .: y = Z . i )
thus y = y ; :: 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 object 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 object ; :: 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 S₁[i,Y . 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 object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or Y . i is finite )
assume i in I ; :: thesis: Y . i is finite
then S₁[i,Y . i] by A7;
hence Y . i is finite ; :: thesis: verum

end;

now :: thesis: for i being object st i in I holds
(F .:.: Y) . i = Z . i

let i be object ; :: thesis: ( i in I implies (F .:.: Y) . i = Z . i )
assume A8: i in I ; :: thesis: (F .:.: Y) . i = Z . i
then S₁[i,Y . i] by A7;
hence (F .:.: Y) . i = Z . i by A8, PBOOLE:def 20; :: thesis: verum

end;

hence F .:.: Y = Z ; :: thesis: verum