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) ) ) )

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;

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 that 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;

end;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 ) )

hence
IT . i = coprod (i,X)
by A2, Def2; :: thesis: verum( ( 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 ) )

i in {i} by TARSKI:def 1;

hence x in IT . i by A3, A6, ZFMISC_1:def 2; :: thesis: verum

end;( 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 )

given a being set such that A6:
( a in X . i & x = [a,i] )
; :: thesis: x in IT . i( 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;( 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

i in {i} by TARSKI:def 1;

hence x in IT . i by A3, A6, ZFMISC_1:def 2; :: thesis: verum

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}:]

hence
IT = coprod
by A9, CARD_3:def 3; :: thesis: verumIT . 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 ;

.= [:(X . x),{x}:] by A12, TARSKI:2 ; :: thesis: verum

end;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) ) )

thus IT . x =
coprod (x,X)
by A8, A10
( ( 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) ) )

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;hereby :: thesis: ( a in [:(X . x),{x}:] implies a in coprod (x,X) )

assume
a in [:(X . x),{x}:]
; :: thesis: 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;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

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

.= [:(X . x),{x}:] by A12, TARSKI:2 ; :: thesis: verum