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 4; :: 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 4;
then A3: IT . i = [:(X . i),{i}:] by A1, CARD_3:def 3;

now

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 set such that
A4: a in X . i and
A5: ( b in {i} & x = [a,b] ) by A3, ZFMISC_1:def 2;
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 4;

now

let x be set ; :: 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 by PARTFUN1:def 4;

A12: now

let a be set ; :: 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 set 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 A7, A8, A9, A10
.= [:(X . x),{x}:] by A12, TARSKI:2 ; :: thesis: verum

end;

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