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 A17: 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 A18: 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
A19: for A being object st A in bool the carrier' of C holds
F1 . A = F2 . A
proof
let A be object ; :: 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 A17
.= F2 . A by A18 ;
hence F1 . A = F2 . A ; :: 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