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]

proof

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

end;

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 that
A1: [u,v1] in f and
A2: [u,v2] in f ; :: thesis: 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 = [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 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 = [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, MCART_1:def 2
.= { o where o is Object of C : for a being Attribute of C st a in A9 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
.= [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, MCART_1:def 1
.= A9 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: for x being set st x in dom f holds
x in bool the carrier' of C

proof

let x be set ; :: 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 set such that
A8: [x,y] in f by RELAT_1:def 4;
consider A being Subset of the carrier' of C such that
A9: [x,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 A8;
x = [x,y] `1 by MCART_1:def 1
.= A by A9, MCART_1:def 1 ;
hence x in bool the carrier' of C ; :: thesis: verum

end;

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

proof

let x be set ; :: 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, { o where o is Object of C : for a being Attribute of C st a in x holds
o is-connected-with a } ] in f ;
hence x in dom f by RELAT_1:def 4; :: thesis: verum

end;

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

proof

let y be set ; :: 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 set such that
A11: [x,y] in f by RELAT_1:def 5;
consider A being Subset of the carrier' of C such that
A12: [x,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 A11;
A13: { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } c= the carrier of C

proof

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

end;

y = [x,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 A12, MCART_1:def 2 ;
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 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; :: 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
A14: [A,y] in f by A10, RELAT_1:def 4;
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 by MCART_1:def 2
.= { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } by A15, MCART_1:def 2 ;
A = [A,y] `1 by MCART_1:def 1
.= A9 by A15, MCART_1:def 1 ;
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; :: thesis: 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 } ; :: thesis: verum