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 & b in {i} ) and
A5: 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 A4, A5, TARSKI:def 1; :: thesis: verum

end;

given a being set such that A6: a in X . i and
A7: x = [a,i] ; :: thesis: x in IT . i
i in {i} by TARSKI:def 1;
hence x in IT . i by A3, A6, A7, ZFMISC_1:def 2; :: thesis: verum

end;

hence IT . i = coprod i,X by A2, Def2; :: thesis: verum

end;

assume that
A9: dom IT = I and
A8: for i being set st i in I holds
IT . i = coprod i,X ; :: thesis: IT = coprod
A10: dom IT = dom X by A9, PARTFUN1:def 4;

now

let x be set ; :: thesis: ( x in dom X implies IT . x = [:(X . x),{x}:] )
assume A11: x in dom X ; :: thesis: IT . x = [:(X . x),{x}:]
then A12: x in I by PARTFUN1:def 4;

A13: 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 consider b being set such that
A14: b in X . x and
A15: a = [b,x] by A12, Def2;
x in {x} by TARSKI:def 1;
hence a in [:(X . x),{x}:] by A14, A15, 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
A16: ( a1 in X . x & a2 in {x} ) and
A17: a = [a1,a2] by ZFMISC_1:def 2;
a2 = x by A16, TARSKI:def 1;
hence a in coprod x,X by A12, A16, A17, Def2; :: thesis: verum

end;

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

end;

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