let F1, F2 be Function of (bool the carrier' of C),(bool the carrier of C); :: thesis: ( ( for A being Subset of the carrier' of C holds F1 . 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 F2 . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ) implies F1 = F2 )
assume A19: for A being Subset of the carrier' of C holds F1 . 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: ( ex A being Subset of the carrier' of C st not F2 . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } or F1 = F2 )
assume A20: for A being Subset of the carrier' of C holds F2 . 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: F1 = F2
A21: for A being set st A in bool the carrier' of C holds
F1 . A = F2 . A

proof

let A be set ; :: thesis: ( A in bool the carrier' of C implies F1 . A = F2 . A )
assume A in bool the carrier' of C ; :: thesis: F1 . A = F2 . A
then reconsider A = A as Subset of the carrier' of C ;
F1 . 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 A19
.= F2 . A by A20 ;
hence F1 . A = F2 . A ; :: thesis: verum

end;

A22: dom F1 = bool the carrier' of C by FUNCT_2:def 1;
dom F2 = bool the carrier' of C by FUNCT_2:def 1;
hence F1 = F2 by A21, A22, FUNCT_1:9; :: thesis: verum