let IT be Function; :: thesis: ( IT = coprod iff ( dom IT = I & ( for i being set st i in I holds
IT . i = coprod (i,X) ) ) )

hereby :: thesis: ( dom IT = I & ( for i being set st i in I holds
IT . i = coprod (i,X) ) implies IT = coprod )
assume A1: IT = disjoin X ; :: thesis: ( dom IT = I & ( for i being set st i in I holds
IT . i = coprod (i,X) ) )

hence dom IT = I by PARTFUN1:def 2; :: thesis: for i being set st i in I holds
IT . i = coprod (i,X)

let i be set ; :: thesis: ( i in I implies IT . i = coprod (i,X) )
assume A2: i in I ; :: thesis: IT . i = coprod (i,X)
then i in dom X by PARTFUN1:def 2;
then A3: IT . i = [:(X . i),{i}:] by ;
now :: thesis: for x being set holds
( ( x in IT . i implies ex a being set st
( a in X . i & x = [a,i] ) ) & ( ex a being set st
( a in X . i & x = [a,i] ) implies x in IT . i ) )
let x be set ; :: thesis: ( ( x in IT . i implies ex a being set st
( a in X . i & x = [a,i] ) ) & ( ex a being set st
( a in X . i & x = [a,i] ) implies x in IT . i ) )

hereby :: thesis: ( ex a being set st
( a in X . i & x = [a,i] ) implies x in IT . i )
assume x in IT . i ; :: thesis: ex a being set st
( a in X . i & x = [a,i] )

then consider a, b being object such that
A4: a in X . i and
A5: ( b in {i} & x = [a,b] ) by ;
reconsider a = a as set by TARSKI:1;
take a = a; :: thesis: ( a in X . i & x = [a,i] )
thus a in X . i by A4; :: thesis: x = [a,i]
thus x = [a,i] by ; :: thesis: verum
end;
given a being set such that A6: ( a in X . i & x = [a,i] ) ; :: thesis: x in IT . i
i in {i} by TARSKI:def 1;
hence x in IT . i by ; :: thesis: verum
end;
hence IT . i = coprod (i,X) by ; :: thesis: verum
end;
assume that
A7: dom IT = I and
A8: for i being set st i in I holds
IT . i = coprod (i,X) ; :: thesis: IT = coprod
A9: dom IT = dom X by ;
now :: thesis: for x being object st x in dom X holds
IT . x = [:(X . x),{x}:]
let x be object ; :: thesis: ( x in dom X implies IT . x = [:(X . x),{x}:] )
assume A10: x in dom X ; :: thesis: IT . x = [:(X . x),{x}:]
then A11: x in I ;
A12: now :: thesis: for a being object holds
( ( a in coprod (x,X) implies a in [:(X . x),{x}:] ) & ( a in [:(X . x),{x}:] implies a in coprod (x,X) ) )
let a be object ; :: thesis: ( ( a in coprod (x,X) implies a in [:(X . x),{x}:] ) & ( a in [:(X . x),{x}:] implies a in coprod (x,X) ) )
hereby :: thesis: ( a in [:(X . x),{x}:] implies a in coprod (x,X) )
assume a in coprod (x,X) ; :: thesis: a in [:(X . x),{x}:]
then A13: ex b being set st
( b in X . x & a = [b,x] ) by ;
x in {x} by TARSKI:def 1;
hence a in [:(X . x),{x}:] by ; :: thesis: verum
end;
assume a in [:(X . x),{x}:] ; :: thesis: a in coprod (x,X)
then consider a1, a2 being object such that
A14: a1 in X . x and
A15: a2 in {x} and
A16: a = [a1,a2] by ZFMISC_1:def 2;
a2 = x by ;
hence a in coprod (x,X) by ; :: thesis: verum
end;
thus IT . x = coprod (x,X) by
.= [:(X . x),{x}:] by ; :: thesis: verum
end;
hence IT = coprod by ; :: thesis: verum