let IT be Function; ( IT = coprod iff ( dom IT = I & ( for i being set st i in I holds
IT . i = coprod (i,X) ) ) )
hereby ( 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
;
( 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;
for i being set st i in I holds
IT . i = coprod (i,X)let i be
set ;
( i in I implies IT . i = coprod (i,X) )assume A2:
i in I
;
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 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 ) )end; hence
IT . i = coprod (
i,
X)
by A2, Def2;
verum
end;
assume that
A7:
dom IT = I
and
A8:
for i being set st i in I holds
IT . i = coprod (i,X)
; IT = coprod
A9:
dom IT = dom X
by A7, PARTFUN1:def 2;
now for x being object st x in dom X holds
IT . x = [:(X . x),{x}:]let x be
object ;
( x in dom X implies IT . x = [:(X . x),{x}:] )assume A10:
x in dom X
;
IT . x = [:(X . x),{x}:]then A11:
x in I
;
A12:
now 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 ;
( ( a in coprod (x,X) implies a in [:(X . x),{x}:] ) & ( a in [:(X . x),{x}:] implies a in coprod (x,X) ) )assume
a in [:(X . x),{x}:]
;
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;
verum end; thus IT . x =
coprod (
x,
X)
by A8, A10
.=
[:(X . x),{x}:]
by A12, TARSKI:2
;
verum end;
hence
IT = coprod
by A9, CARD_3:def 3; verum