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

proof

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