let I be set ; :: thesis: for F being ManySortedFunction of
for Z being ManySortedSet of st Z is finite-yielding & Z c= rngs F holds
ex Y being ManySortedSet of st
( Y c= doms F & Y is finite-yielding & F .:.: Y = Z )
let F be ManySortedFunction of ; :: thesis: for Z being ManySortedSet of st Z is finite-yielding & Z c= rngs F holds
ex Y being ManySortedSet of st
( Y c= doms F & Y is finite-yielding & F .:.: Y = Z )
let Z be ManySortedSet of ; :: thesis: ( Z is finite-yielding & Z c= rngs F implies ex Y being ManySortedSet of 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 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] )
assume A4: i in I ; :: thesis: ex j being set st S₁[i,j]
then A5: Z . i is finite by A1, LL1;
reconsider f = F . i as Function ;
rng f = (rngs F) . i by A4, Th13;
then Z . i c= rng f by A2, A4, PBOOLE:def 5;
then consider y being set such that
A6: ( y c= dom f & y is finite & f .: y = Z . i ) by A5, ORDERS_1:195;
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 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 5 :: thesis: ( not i in I or Y . i c= (doms F) . i )
assume i in I ; :: thesis: Y . i c= (doms F) . i
then consider f being Function such that
A8: ( f = F . i & Y . i c= (doms F) . i & Y . i is finite & f .: (Y . i) = Z . i ) by A7;
thus Y . i c= (doms F) . i by A8; :: 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 consider f being Function such that
A9: ( f = F . i & Y . i c= (doms F) . i & Y . i is finite & f .: (Y . i) = Z . i ) by A7;
thus Y . i is finite by A9; :: thesis: verum

end;

now

let i be set ; :: thesis: ( i in I implies (F .:.: Y) . i = Z . i )
assume A10: i in I ; :: thesis: (F .:.: Y) . i = Z . i
then consider f being Function such that
A11: ( f = F . i & Y . i c= (doms F) . i & Y . i is finite & f .: (Y . i) = Z . i ) by A7;
thus (F .:.: Y) . i = Z . i by A10, A11, PBOOLE:def 25; :: thesis: verum

end;

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