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 object 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 object 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 object st [u,v1] in f & [u,v2] in f holds
v1 = v2
proof
let u,
v1,
v2 be
object ;
( [u,v1] in f & [u,v2] in f implies v1 = v2 )
assume that A1:
[u,v1] in f
and A2:
[u,v2] in f
;
v1 = v2
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 } ]
by A1;
A4:
v1 =
[u,v1] `2
.=
[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
.=
{ o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }
;
consider A9 being
Subset of the
carrier' of
C such that A5:
[u,v2] = [A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ]
by A2;
A6:
v2 =
[u,v2] `2
.=
[A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ] `2
by A5
.=
[A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ] `2
.=
{ o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a }
;
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
.=
[u,v1] `1
by A3
.=
u
.=
[u,v2] `1
.=
[A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ] `1
by A5
.=
A9
;
hence
v1 = v2
by A4, A6;
verum
end;
then reconsider f = f as Function by FUNCT_1:def 1;
A7:
for x being object st x in dom f holds
x in bool the carrier' of C
for x being object st x in bool the carrier' of C holds
x in dom f
then A10:
dom f = bool the carrier' of C
by A7, TARSKI:2;
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 A10, FUNCT_2:def 1, RELSET_1:4;
take
f
; 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 }
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;
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
object such that A14:
[A,y] in f
by A10, XTUPLE_0:def 12;
consider A9 being
Subset of the
carrier' of
C such that A15:
[A,y] = [A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ]
by A14;
A16:
y =
[A,y] `2
.=
[A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ] `2
by A15
.=
{ o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a }
;
A =
[A,y] `1
.=
[A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ] `1
by A15
.=
A9
;
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 A10, A14, A16, FUNCT_1:def 2;
verum
end;
hence
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 }
; verum