set P = pcs-union C;
set IR = the InternalRel of (pcs-union C);
set CP = the carrier of (pcs-union C);
set CA = Carrier C;
A1:
the carrier of (pcs-union C) = Union (Carrier C)
by Def36;
A2:
the InternalRel of (pcs-union C) = Union (pcs-InternalRels C)
by Def36;
A3:
dom (pcs-InternalRels C) = I
by PARTFUN1:def 2;
let x be object ; RELAT_2:def 1,ORDERS_2:def 2 ( not x in the carrier of (pcs-union C) or [^,^] in the InternalRel of (pcs-union C) )
assume
x in the carrier of (pcs-union C)
; [^,^] in the InternalRel of (pcs-union C)
then consider P being set such that
A4:
x in P
and
A5:
P in rng (Carrier C)
by A1, TARSKI:def 4;
consider i being object such that
A6:
i in dom (Carrier C)
and
A7:
(Carrier C) . i = P
by A5, FUNCT_1:def 3;
A8:
ex R being 1-sorted st
( R = C . i & (Carrier C) . i = the carrier of R )
by A6, PRALG_1:def 15;
reconsider I = I as non empty set by A6;
reconsider i = i as Element of I by A6;
reconsider C = C as reflexive-yielding () ManySortedSet of I ;
A9:
(pcs-InternalRels C) . i = the InternalRel of (C . i)
by Def6;
the InternalRel of (C . i) is_reflexive_in the carrier of (C . i)
by ORDERS_2:def 2;
then A10:
[x,x] in the InternalRel of (C . i)
by A4, A7, A8;
the InternalRel of (C . i) in rng (pcs-InternalRels C)
by A3, A9, FUNCT_1:3;
hence
[^,^] in the InternalRel of (pcs-union C)
by A2, A10, TARSKI:def 4; verum