let i be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not i in proj1 (Coprod A) or (Coprod A) . i is set )
assume i in dom (Coprod A) ; :: thesis: (Coprod A) . i is set
then ex F being Function of (A . i),(Union (coprod A)) st
( (Coprod A) . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) ) by Def10;
hence (Coprod A) . i is set ; :: thesis: verum