set CA = Carrier C;
set IRA = pcs-InternalRels C;
set TRA = pcs-ToleranceRels C;
set D = Union (Carrier C);
set IR = Union (pcs-InternalRels C);
set TR = Union (pcs-ToleranceRels C);
A1:
dom (Carrier C) = I
by PARTFUN1:def 2;
Union (pcs-InternalRels C) c= [:(Union (Carrier C)),(Union (Carrier C)):]
proof
let x be
object ;
TARSKI:def 3 ( not x in Union (pcs-InternalRels C) or x in [:(Union (Carrier C)),(Union (Carrier C)):] )
assume
x in Union (pcs-InternalRels C)
;
x in [:(Union (Carrier C)),(Union (Carrier C)):]
then consider P being
set such that A2:
x in P
and A3:
P in rng (pcs-InternalRels C)
by TARSKI:def 4;
consider i being
object such that A4:
i in dom (pcs-InternalRels C)
and A5:
(pcs-InternalRels C) . i = P
by A3, FUNCT_1:def 3;
consider R being
RelStr such that A6:
R = C . i
and A7:
(pcs-InternalRels C) . i = the
InternalRel of
R
by A4, Def5;
consider x1,
x2 being
object such that A8:
x = [x1,x2]
and A9:
x1 in the
carrier of
R
and A10:
x2 in the
carrier of
R
by A2, A5, A7, RELSET_1:2;
ex
S being
1-sorted st
(
S = C . i &
(Carrier C) . i = the
carrier of
S )
by A4, PRALG_1:def 15;
then A11:
the
carrier of
R in rng (Carrier C)
by A1, A4, A6, FUNCT_1:def 3;
then A12:
x1 in union (rng (Carrier C))
by A9, TARSKI:def 4;
x2 in union (rng (Carrier C))
by A10, A11, TARSKI:def 4;
hence
x in [:(Union (Carrier C)),(Union (Carrier C)):]
by A8, A12, ZFMISC_1:87;
verum
end;
then reconsider IR = Union (pcs-InternalRels C) as Relation of (Union (Carrier C)) ;
Union (pcs-ToleranceRels C) c= [:(Union (Carrier C)),(Union (Carrier C)):]
proof
let x be
object ;
TARSKI:def 3 ( not x in Union (pcs-ToleranceRels C) or x in [:(Union (Carrier C)),(Union (Carrier C)):] )
assume
x in Union (pcs-ToleranceRels C)
;
x in [:(Union (Carrier C)),(Union (Carrier C)):]
then consider P being
set such that A13:
x in P
and A14:
P in rng (pcs-ToleranceRels C)
by TARSKI:def 4;
consider i being
object such that A15:
i in dom (pcs-ToleranceRels C)
and A16:
(pcs-ToleranceRels C) . i = P
by A14, FUNCT_1:def 3;
consider R being
TolStr such that A17:
R = C . i
and A18:
(pcs-ToleranceRels C) . i = the
ToleranceRel of
R
by A15, Def19;
consider x1,
x2 being
object such that A19:
x = [x1,x2]
and A20:
x1 in the
carrier of
R
and A21:
x2 in the
carrier of
R
by A13, A16, A18, RELSET_1:2;
ex
S being
1-sorted st
(
S = C . i &
(Carrier C) . i = the
carrier of
S )
by A15, PRALG_1:def 15;
then A22:
the
carrier of
R in rng (Carrier C)
by A1, A15, A17, FUNCT_1:def 3;
then A23:
x1 in union (rng (Carrier C))
by A20, TARSKI:def 4;
x2 in union (rng (Carrier C))
by A21, A22, TARSKI:def 4;
hence
x in [:(Union (Carrier C)),(Union (Carrier C)):]
by A19, A23, ZFMISC_1:87;
verum
end;
then reconsider TR = Union (pcs-ToleranceRels C) as Relation of (Union (Carrier C)) ;
take
pcs-Str(# (Union (Carrier C)),IR,TR #)
; ( the carrier of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (Carrier C) & the InternalRel of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (pcs-InternalRels C) & the ToleranceRel of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (pcs-ToleranceRels C) )
thus
( the carrier of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (Carrier C) & the InternalRel of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (pcs-InternalRels C) & the ToleranceRel of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (pcs-ToleranceRels C) )
; verum