defpred S1[ object , object ] means ex F being Function of (A . $1),(Union (coprod A)) st
( $2 = F & ( for x being object st x in A . $1 holds
F . x = [x,$1] ) );
A1:
for i being object st i in I holds
ex j being object st S1[i,j]
proof
let i be
object ;
( i in I implies ex j being object st S1[i,j] )
assume A2:
i in I
;
ex j being object st S1[i,j]
defpred S2[
object ,
object ]
means $2
= [$1,i];
A3:
for
x being
object st
x in A . i holds
ex
y being
object st
(
y in Union (coprod A) &
S2[
x,
y] )
proof
let x be
object ;
( x in A . i implies ex y being object st
( y in Union (coprod A) & S2[x,y] ) )
assume A4:
x in A . i
;
ex y being object st
( y in Union (coprod A) & S2[x,y] )
take y =
[x,i];
( y in Union (coprod A) & S2[x,y] )
set Z =
coprod (
i,
A);
A5:
y in coprod (
i,
A)
by A2, A4, MSAFREE:def 2;
A6:
dom (coprod A) = I
by PARTFUN1:def 2;
(coprod A) . i = coprod (
i,
A)
by A2, MSAFREE:def 3;
then
coprod (
i,
A)
in rng (coprod A)
by A2, A6, FUNCT_1:3;
hence
y in Union (coprod A)
by A5, TARSKI:def 4;
S2[x,y]
thus
S2[
x,
y]
;
verum
end;
ex
F being
Function of
(A . i),
(Union (coprod A)) st
for
x being
object st
x in A . i holds
S2[
x,
F . x]
from FUNCT_2:sch 1(A3);
hence
ex
j being
object st
S1[
i,
j]
;
verum
end;
ex f being ManySortedSet of I st
for i being object st i in I holds
S1[i,f . i]
from PBOOLE:sch 3(A1);
hence
ex b1 being ManySortedSet of I st
for i being object st i in I holds
ex F being Function of (A . i),(Union (coprod A)) st
( b1 . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) )
; verum