set f = { [O,{ a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] where O is Subset of the carrier of C : verum } ;
for u being set st u in { [O,{ a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] where O is Subset of the carrier of C : verum } holds
ex v, w being set st u = [v,w]
then reconsider f = { [O,{ a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] where O 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 O being
Subset of the
carrier of
C such that A3:
[u,v1] = [O,{ a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ]
;
A4:
v1 =
[O,{ a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] `2
by A3, MCART_1:def 2
.=
{ a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
by MCART_1:def 2
;
consider O' being
Subset of the
carrier of
C such that A5:
[u,v2] = [O',{ a where a is Attribute of C : for o being Object of C st o in O' holds
o is-connected-with a } ]
by A2;
A6:
v2 =
[O',{ a where a is Attribute of C : for o being Object of C st o in O' holds
o is-connected-with a } ] `2
by A5, MCART_1:def 2
.=
{ a where a is Attribute of C : for o being Object of C st o in O' holds
o is-connected-with a }
by MCART_1:def 2
;
O =
[O,{ a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] `1
by MCART_1:def 1
.=
u
by A3, MCART_1:def 1
.=
[O',{ a where a is Attribute of C : for o being Object of C st o in O' holds
o is-connected-with a } ] `1
by A5, MCART_1:def 1
.=
O'
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 O being Subset of the carrier of C holds f . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
proof
let O be
Subset of the
carrier of
C;
:: thesis: f . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
consider y being
set such that A16:
[O,y] in f
by A7, RELAT_1:def 4;
consider O' being
Subset of the
carrier of
C such that A17:
[O,y] = [O',{ a where a is Attribute of C : for o being Object of C st o in O' holds
o is-connected-with a } ]
by A16;
A18:
O =
[O,y] `1
by MCART_1:def 1
.=
O'
by A17, MCART_1:def 1
;
y =
[O,y] `2
by MCART_1:def 2
.=
{ a where a is Attribute of C : for o being Object of C st o in O' holds
o is-connected-with a }
by A17, MCART_1:def 2
;
hence
f . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
by A7, A16, A18, FUNCT_1:def 4;
:: thesis: verum
end;
take
f
; :: thesis: for O being Subset of the carrier of C holds f . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
thus
for O being Subset of the carrier of C holds f . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
by A15; :: thesis: verum