set f = { [A,{ o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] where A is Subset of the carrier' of C : verum } ;
for u being set st u in { [A,{ o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] where A is Subset of the carrier' of C : verum } holds
ex v, w being set st u = [v,w]
then reconsider f = { [A,{ o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] where A is Subset of the carrier' of C : verum } as Relation by RELAT_1:def 1;
for u, v1, v2 being set st [u,v1] in f & [u,v2] in f holds
v1 = v2
proof
let u,
v1,
v2 be
set ;
:: thesis: ( [u,v1] in f & [u,v2] in f implies v1 = v2 )
assume A2:
(
[u,v1] in f &
[u,v2] in f )
;
:: thesis: v1 = v2
then consider A being
Subset of the
carrier' of
C such that A3:
[u,v1] = [A,{ o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ]
;
A4:
v1 =
[A,{ o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] `2
by A3, MCART_1:def 2
.=
{ o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }
by MCART_1:def 2
;
consider A' being
Subset of the
carrier' of
C such that A5:
[u,v2] = [A',{ o where o is Object of C : for a being Attribute of C st a in A' holds
o is-connected-with a } ]
by A2;
A6:
v2 =
[A',{ o where o is Object of C : for a being Attribute of C st a in A' holds
o is-connected-with a } ] `2
by A5, MCART_1:def 2
.=
{ o where o is Object of C : for a being Attribute of C st a in A' holds
o is-connected-with a }
by MCART_1:def 2
;
A =
[A,{ o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] `1
by MCART_1:def 1
.=
u
by A3, MCART_1:def 1
.=
[A',{ o where o is Object of C : for a being Attribute of C st a in A' holds
o is-connected-with a } ] `1
by A5, MCART_1:def 1
.=
A'
by MCART_1:def 1
;
hence
v1 = v2
by A4, A6;
:: thesis: verum
end;
then reconsider f = f as Function by FUNCT_1:def 1;
A7:
dom f = bool the carrier' of C
rng f c= bool the carrier of C
then reconsider f = f as Function of (bool the carrier' of C),(bool the carrier of C) by A7, FUNCT_2:def 1, RELSET_1:11;
A15:
for A being Subset of the carrier' of C holds f . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }
proof
let A be
Subset of the
carrier' of
C;
:: thesis: f . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }
consider y being
set such that A16:
[A,y] in f
by A7, RELAT_1:def 4;
consider A' being
Subset of the
carrier' of
C such that A17:
[A,y] = [A',{ o where o is Object of C : for a being Attribute of C st a in A' holds
o is-connected-with a } ]
by A16;
A18:
A =
[A,y] `1
by MCART_1:def 1
.=
A'
by A17, MCART_1:def 1
;
y =
[A,y] `2
by MCART_1:def 2
.=
{ o where o is Object of C : for a being Attribute of C st a in A' holds
o is-connected-with a }
by A17, MCART_1:def 2
;
hence
f . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }
by A7, A16, A18, FUNCT_1:def 4;
:: thesis: verum
end;
take
f
; :: thesis: for A being Subset of the carrier' of C holds f . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }
thus
for A being Subset of the carrier' of C holds f . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }
by A15; :: thesis: verum