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 A17: 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 A18: 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
A19: for O being object st O in bool the carrier of C holds
F1 . O = F2 . O

proof

let O be object ; :: 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 A17
.= F2 . O by A18 ;
hence F1 . O = F2 . O ; :: thesis: verum

end;

( dom F1 = bool the carrier of C & dom F2 = bool the carrier of C ) by FUNCT_2:def 1;
hence F1 = F2 by A19, FUNCT_1:2; :: thesis: verum