defpred S₁[ 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 S₁[i,j]

proof

let i be object ; :: thesis: ( i in I implies ex j being object st S₁[i,j] )
assume A2: i in I ; :: thesis: ex j being object st S₁[i,j]
defpred S₂[ 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) & S₂[x,y] )

proof

let x be object ; :: thesis: ( x in A . i implies ex y being object st
( y in Union (coprod A) & S₂[x,y] ) )
assume A4: x in A . i ; :: thesis: ex y being object st
( y in Union (coprod A) & S₂[x,y] )
take y = [x,i]; :: thesis: ( y in Union (coprod A) & S₂[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; :: thesis: S₂[x,y]
thus S₂[x,y] ; :: thesis: verum

end;

ex F being Function of (A . i),(Union (coprod A)) st
for x being object st x in A . i holds
S₂[x,F . x] from FUNCT_2:sch 1(A3);
hence ex j being object st S₁[i,j] ; :: thesis: verum

end;

ex f being ManySortedSet of I st
for i being object st i in I holds
S₁[i,f . i] from PBOOLE:sch 3(A1);
hence ex b₁ 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
( b₁ . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) ) ; :: thesis: verum