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 object 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 object st u = [v,w]

proof

let u be object ; :: thesis: ( 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 } implies ex v, w being object st u = [v,w] )
assume 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 } ; :: thesis: ex v, w being object st u = [v,w]
then ex O being Subset of the carrier of C st u = [O, { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] ;
hence ex v, w being object st u = [v,w] ; :: thesis: verum

end;

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 object st [u,v1] in f & [u,v2] in f holds
v1 = v2

proof

let u, v1, v2 be object ; :: thesis: ( [u,v1] in f & [u,v2] in f implies v1 = v2 )
assume that
A1: [u,v1] in f and
A2: [u,v2] in f ; :: thesis: v1 = v2
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 } ] by A1;
A4: v1 = [u,v1] `2
.= [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
.= { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ;
consider O9 being Subset of the carrier of C such that
A5: [u,v2] = [O9, { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ] by A2;
A6: v2 = [u,v2] `2
.= [O9, { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ] `2 by A5
.= { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ;
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
.= [u,v1] `1 by A3
.= u
.= [u,v2] `1
.= [O9, { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ] `1 by A5
.= O9 ;
hence v1 = v2 by A4, A6; :: thesis: 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

proof

let x be object ; :: thesis: ( x in dom f implies x in bool the carrier of C )
assume x in dom f ; :: thesis: x in bool the carrier of C
then consider y being object such that
A8: [x,y] in f by XTUPLE_0:def 12;
consider O being Subset of the carrier of C such that
A9: [x,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 A8;
x = [x,y] `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 A9
.= O ;
hence x in bool the carrier of C ; :: thesis: verum

end;

for x being object st x in bool the carrier of C holds
x in dom f

proof

let x be object ; :: thesis: ( x in bool the carrier of C implies x in dom f )
assume x in bool the carrier of C ; :: thesis: x in dom f
then reconsider x = x as Subset of the carrier of C ;
[x, { a where a is Attribute of C : for o being Object of C st o in x holds
o is-connected-with a } ] in f ;
hence x in dom f by XTUPLE_0:def 12; :: thesis: verum

end;

then A10: dom f = bool the carrier of C by A7, TARSKI:2;
rng f c= bool the carrier' of C

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in bool the carrier' of C )
assume y in rng f ; :: thesis: y in bool the carrier' of C
then consider x being object such that
A11: [x,y] in f by XTUPLE_0:def 13;
consider O being Subset of the carrier of C such that
A12: [x,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 A11;
A13: { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } c= the carrier' of C

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } or u in the carrier' of C )
assume u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; :: thesis: u in the carrier' of C
then ex u9 being Attribute of C st
( u9 = u & ( for o being Object of C st o in O holds
o is-connected-with u9 ) ) ;
hence u in the carrier' of C ; :: thesis: verum

end;

y = [x,y] `2
.= [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 A12
.= { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ;
hence y in bool the carrier' of C by A13; :: thesis: verum

end;

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 ; :: 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 }
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 object such that
A14: [O,y] in f by A10, XTUPLE_0:def 12;
consider O9 being Subset of the carrier of C such that
A15: [O,y] = [O9, { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ] by A14;
A16: y = [O,y] `2
.= [O9, { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ] `2 by A15
.= { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ;
O = [O,y] `1
.= [O9, { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ] `1 by A15
.= O9 ;
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 A10, A14, A16, FUNCT_1:def 2; :: thesis: verum

end;

hence 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 } ; :: thesis: verum