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 A1, CARD_3:def 3;

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 A3, ZFMISC_1:def 2;
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 A5, TARSKI:def 1; :: 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 A3, A6, ZFMISC_1:def 2; :: thesis: verum

end;

hence IT . i = coprod (i,X) by A2, Def2; :: 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 A7, PARTFUN1:def 2;

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 A11, Def2;
x in {x} by TARSKI:def 1;
hence a in [:(X . x),{x}:] by A13, ZFMISC_1:def 2; :: 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 A15, TARSKI:def 1;
hence a in coprod (x,X) by A11, A14, A16, Def2; :: thesis: verum

end;

thus IT . x = coprod (x,X) by A8, A10
.= [:(X . x),{x}:] by A12, TARSKI:2 ; :: thesis: verum

end;

hence IT = coprod by A9, CARD_3:def 3; :: thesis: verum